Module Global

This module defines the global environment of Rocq. 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
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 set_rewrite_rules_allowed : bool -> unit
val rewrite_rules_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 : UVars.UContext.t -> unit
val fill_opaque : Safe_typing.opaque_certificate -> unit
val add_rewrite_rules : Names.Id.t -> Declarations.rewrite_rules_body -> unit
val add_constraints : Univ.Constraints.t -> unit

Extra universe constraints

val push_context_set : Univ.ContextSet.t -> unit

Non-interactive modules and module types

Sections

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

Interactive modules and module types

val start_module : Names.Id.t -> Names.ModPath.t
val start_modtype : Names.Id.t -> Names.ModPath.t
Queries in the global environment
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 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
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_curmod_library : unit -> bool
val is_polymorphic : Names.GlobRef.t -> bool
val is_template_polymorphic : Names.GlobRef.t -> bool
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 : Conv_oracle.evaluable -> 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