Module `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 env_is_initial : unit -> bool
val universes : unit -> UGraph.t
val universes_lbound : unit -> Univ.Level.t
val named_context_val : unit -> Environ.named_context_val
val named_context : unit -> Constr.named_context

Enriching the global environment

val set_engagement : Declarations.engagement -> 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 make_sprop_cumulative : unit -> unit
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 : (Names.Name.t array * Univ.UContext.t) -> unit
val export_private_constants : Safe_typing.private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list
val add_constant : Names.Id.t -> Safe_typing.global_declaration -> Names.Constant.t
val add_private_constant : Names.Id.t -> Safe_typing.side_effect_declaration -> Names.Constant.t * Safe_typing.private_constants
val add_mind : Names.Id.t -> Entries.mutual_inductive_entry -> Names.MutInd.t
val add_constraints : Univ.Constraint.t -> unit: Extra universe constraints

val push_context_set : 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.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.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 -> Opaqueproof.opaque 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
val opaque_tables : unit -> Opaqueproof.opaquetab
val body_of_constant : Opaqueproof.indirect_accessor -> Names.Constant.t -> (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.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 : Opaqueproof.indirect_accessor -> Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option: Same as body_of_constant but on Declarations.constant_body.

Compiled libraries

val start_library : Names.DirPath.t -> Names.ModPath.t
val export : ?⁠except:Future.UUIDSet.t -> output_native_objects:bool -> Names.DirPath.t -> Names.ModPath.t * Safe_typing.compiled_library * Safe_typing.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 join_safe_environment : ?⁠except:Future.UUIDSet.t -> unit -> unit
val is_joined_environment : unit -> bool
val is_polymorphic : Names.GlobRef.t -> bool
val is_template_polymorphic : Names.GlobRef.t -> bool
val is_template_checked : 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