Global (coq-core.Global)

val safe_env : unit -> Safe_typing.safe_environment

val env : unit -> Environ.env

val env_is_initial : unit -> bool

val universes : unit -> UGraph.t

val universes_lbound : unit -> UGraph.Bound.t

val named_context_val : unit -> Environ.named_context_val

val named_context : unit -> Constr.named_context

Enriching the global environment

val set_impredicative_set : bool -> unit

Changing the (im)predicativity of the system

val set_indices_matter : bool -> unit

val set_typing_flags : Declarations.typing_flags -> unit

val set_check_guarded : bool -> unit

val set_check_positive : bool -> unit

val set_check_universes : bool -> unit

val typing_flags : unit -> Declarations.typing_flags

val set_cumulative_sprop : bool -> unit

val is_cumulative_sprop : unit -> bool

val set_allow_sprop : bool -> unit

val sprop_allowed : unit -> bool

Variables, Local definitions, constants, inductive types

val push_named_assum : (Names.Id.t * Constr.types) -> unit

val push_named_def : (Names.Id.t * Entries.section_def_entry) -> unit

val push_section_context : Univ.UContext.t -> unit

val export_private_constants : Safe_typing.private_constants -> Safe_typing.exported_private_constant list

val add_constant : ?typing_flags:Declarations.typing_flags -> Names.Id.t -> Safe_typing.global_declaration -> Names.Constant.t

val fill_opaque : Safe_typing.opaque_certificate -> unit

val add_private_constant : Names.Id.t -> Univ.ContextSet.t -> Safe_typing.side_effect_declaration -> Names.Constant.t * Safe_typing.private_constants

val add_mind : ?typing_flags:Declarations.typing_flags -> Names.Id.t -> Entries.mutual_inductive_entry -> Names.MutInd.t

val add_constraints : Univ.Constraints.t -> unit

Extra universe constraints

val push_context_set : strict:bool -> Univ.ContextSet.t -> unit

Non-interactive modules and module types

val add_module : Names.Id.t -> Entries.module_entry -> Declarations.inline -> Names.ModPath.t * Mod_subst.delta_resolver

val add_modtype : Names.Id.t -> Entries.module_type_entry -> Declarations.inline -> Names.ModPath.t

val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver

Sections

val open_section : unit -> unit

poly is true when the section should be universe polymorphic

val close_section : Summary.frozen -> unit

Close the section and reset the global state to the one at the time when the section what opened.

val sections_are_opened : unit -> bool

Interactive modules and module types

val start_module : Names.Id.t -> Names.ModPath.t

val start_modtype : Names.Id.t -> Names.ModPath.t

val end_module : Summary.frozen -> Names.Id.t -> (Entries.module_struct_entry * Declarations.inline) option -> Names.ModPath.t * Names.MBId.t list * Mod_subst.delta_resolver

val end_modtype : Summary.frozen -> Names.Id.t -> Names.ModPath.t * Names.MBId.t list

val add_module_parameter : Names.MBId.t -> Entries.module_struct_entry -> Declarations.inline -> Mod_subst.delta_resolver

Queries in the global environment

val lookup_named : Names.variable -> Constr.named_declaration

val lookup_constant : Names.Constant.t -> Declarations.constant_body

val lookup_inductive : Names.inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body

val lookup_pinductive : Constr.pinductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body

val lookup_mind : Names.MutInd.t -> Declarations.mutual_inductive_body

val lookup_module : Names.ModPath.t -> Declarations.module_body

val lookup_modtype : Names.ModPath.t -> Declarations.module_type_body

val exists_objlabel : Names.Label.t -> bool

val constant_of_delta_kn : Names.KerName.t -> Names.Constant.t

val mind_of_delta_kn : Names.KerName.t -> Names.MutInd.t

type indirect_accessor = {

access_proof : Opaqueproof.opaque -> (Constr.t * unit Opaqueproof.delayed_universes) option;

}

val force_proof : indirect_accessor -> Opaqueproof.opaque -> Constr.t * unit Opaqueproof.delayed_universes

val body_of_constant : indirect_accessor -> Names.Constant.t -> (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AbstractContext.t) option

Returns the body of the constant if it has any, and the polymorphic context it lives in. For monomorphic constant, the latter is empty, and for polymorphic constants, the term contains De Bruijn universe variables that need to be instantiated.

val body_of_constant_body : indirect_accessor -> Declarations.constant_body -> (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AbstractContext.t) option

Same as body_of_constant but on constant_body.

Compiled libraries

val start_library : Names.DirPath.t -> Names.ModPath.t

val export : output_native_objects:bool -> Names.DirPath.t -> Names.ModPath.t * Safe_typing.compiled_library * Nativelib.native_library

val import : Safe_typing.compiled_library -> Univ.ContextSet.t -> Safe_typing.vodigest -> Names.ModPath.t

Misc

Function to get an environment from the constants part of the global * environment and a given context.

val env_of_context : Environ.named_context_val -> Environ.env

val is_joined_environment : unit -> bool

val is_polymorphic : Names.GlobRef.t -> bool

val is_template_polymorphic : Names.GlobRef.t -> bool

val get_template_polymorphic_variables : Names.GlobRef.t -> Univ.Level.t list

val is_type_in_type : Names.GlobRef.t -> bool

Retroknowledge

val register_inline : Names.Constant.t -> unit

val register_inductive : Names.inductive -> 'a CPrimitives.prim_ind -> unit

Oracle

val set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> unit

Conversion settings

val set_share_reduction : bool -> unit

val set_VM : bool -> unit

val set_native_compiler : bool -> unit

val current_modpath : unit -> Names.ModPath.t

val current_dirpath : unit -> Names.DirPath.t

val with_global : (Environ.env -> Names.DirPath.t -> 'a Univ.in_universe_context_set) -> 'a

val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag