Module Global

val safe_env : unit -> Safe_typing.safe_environment
val env : unit -> Environ.env
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_allow_sprop : bool -> unit
val sprop_allowed : unit -> bool
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 : UVars.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
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
val open_section : unit -> unit

poly is true when the section should be universe polymorphic

val close_section : Summary.Interp.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
val start_module : Names.Id.t -> Names.ModPath.t
val start_modtype : Names.Id.t -> Names.ModPath.t
val end_module : Summary.Interp.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.Interp.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 * UVars.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 * UVars.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
val env_of_context : Environ.named_context_val -> Environ.env
val is_joined_environment : unit -> bool
val is_curmod_library : 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