Global
This module defines the global environment of Coq. The functions below are exactly the same as the ones in Safe_typing
, operating on that global environment. add_*
functions perform name verification, i.e. check that the name given as argument match those provided by Safe_typing
.
val safe_env : unit -> Safe_typing.safe_environment
val env : unit -> Environ.env
val universes : unit -> UGraph.t
val named_context_val : unit -> Environ.named_context_val
val named_context : unit -> Constr.named_context
val set_typing_flags : Declarations.typing_flags -> unit
val typing_flags : unit -> Declarations.typing_flags
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 : 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 -> Entries.constant_entry -> 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_rewrite_rules : Names.Id.t -> Declarations.rewrite_rules_body -> unit
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 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.
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.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
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 -> Opaqueproof.opaque_proofterm option; |
}
val force_proof : indirect_accessor -> Opaqueproof.opaque -> Opaqueproof.opaque_proofterm
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
.
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 * Vmlibrary.compiled_library * Nativelib.native_library
val import : Safe_typing.compiled_library -> Vmlibrary.on_disk -> Safe_typing.vodigest -> Names.ModPath.t
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_polymorphic : Names.GlobRef.t -> bool
val is_template_polymorphic : Names.GlobRef.t -> bool
val is_type_in_type : Names.GlobRef.t -> bool
val register_inline : Names.Constant.t -> unit
val register_inductive : Names.inductive -> 'a CPrimitives.prim_ind -> unit
val set_strategy : Conv_oracle.evaluable -> Conv_oracle.level -> 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