Module Safe_typing

type vodigest =
| Dvo_or_vi of Stdlib.Digest.t
| Dvivo of Stdlib.Digest.t * Stdlib.Digest.t
val digest_match : actual:vodigest -> required:vodigest -> bool
Safe environments
type safe_environment
type section_data
val empty_environment : safe_environment
val is_initial : safe_environment -> bool
val env_of_safe_env : safe_environment -> Environ.env
val sections_of_safe_env : safe_environment -> section_data Section.t option
val structure_body_of_safe_env : safe_environment -> Declarations.structure_body
type safe_transformer0 = safe_environment -> safe_environment
type 'a safe_transformer = safe_environment -> 'a * safe_environment
Stm machinery
type private_constants
val empty_private_constants : private_constants
val is_empty_private_constants : private_constants -> bool
val concat_private : private_constants -> private_constants -> private_constants

concat_private e1 e2 adds the constants of e1 to e2, i.e. constants in e1 must be more recent than those of e2.

val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
val inline_private_constants : Environ.env -> private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_set
val push_private_constants : Environ.env -> private_constants -> Environ.env

Push the constants in the environment if not already there.

val universes_of_private : private_constants -> Univ.ContextSet.t
val is_curmod_library : safe_environment -> bool
val join_safe_environment : ?⁠except:Future.UUIDSet.t -> safe_environment -> safe_environment
val is_joined_environment : safe_environment -> bool
Enriching a safe environment
type global_declaration =
| ConstantEntry : Entries.constant_entry -> global_declaration
| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration
type side_effect_declaration =
| DefinitionEff : Entries.definition_entry -> side_effect_declaration
| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration
type exported_private_constant = Names.Constant.t
val export_private_constants : private_constants -> exported_private_constant list safe_transformer
val add_constant : Names.Label.t -> global_declaration -> Names.Constant.t safe_transformer

returns the main constant

val add_private_constant : Names.Label.t -> side_effect_declaration -> (Names.Constant.t * private_constants) safe_transformer

Similar to add_constant but also returns a certificate

val add_mind : Names.Label.t -> Entries.mutual_inductive_entry -> Names.MutInd.t safe_transformer
val add_module : Names.Label.t -> Entries.module_entry -> Declarations.inline -> (Names.ModPath.t * Mod_subst.delta_resolver) safe_transformer
val add_modtype : Names.Label.t -> Entries.module_type_entry -> Declarations.inline -> Names.ModPath.t safe_transformer
val push_context_set : strict:bool -> Univ.ContextSet.t -> safe_transformer0
val add_constraints : Univ.Constraint.t -> safe_transformer0
val set_engagement : Declarations.engagement -> safe_transformer0

Setting the type theory flavor

val set_indices_matter : bool -> safe_transformer0
val set_typing_flags : Declarations.typing_flags -> safe_transformer0
val set_share_reduction : bool -> safe_transformer0
val set_check_guarded : bool -> safe_transformer0
val set_check_positive : bool -> safe_transformer0
val set_check_universes : bool -> safe_transformer0
val set_VM : bool -> safe_transformer0
val set_native_compiler : bool -> safe_transformer0
val set_allow_sprop : bool -> safe_transformer0
val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
Interactive section functions
val open_section : safe_transformer0
val close_section : safe_transformer0
val sections_are_opened : safe_environment -> bool
val push_named_assum : (Names.Id.t * Constr.types) -> safe_transformer0
val push_named_def : (Names.Id.t * Entries.section_def_entry) -> safe_transformer0
val push_section_context : (Names.Name.t array * Univ.UContext.t) -> safe_transformer0

Add local universes to a polymorphic section

Interactive module functions
val start_module : Names.Label.t -> Names.ModPath.t safe_transformer
val start_modtype : Names.Label.t -> Names.ModPath.t safe_transformer
val add_module_parameter : Names.MBId.t -> Entries.module_struct_entry -> Declarations.inline -> Mod_subst.delta_resolver safe_transformer
val allow_delayed_constants : bool Stdlib.ref

Traditional mode: check at end of module that no future was created.

val end_module : Names.Label.t -> (Entries.module_struct_entry * Declarations.inline) option -> (Names.ModPath.t * Names.MBId.t list * Mod_subst.delta_resolver) safe_transformer
val end_modtype : Names.Label.t -> (Names.ModPath.t * Names.MBId.t list) safe_transformer
val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver safe_transformer
val current_modpath : safe_environment -> Names.ModPath.t
val current_dirpath : safe_environment -> Names.DirPath.t
Libraries : loading and saving compilation units
type compiled_library
type native_library = Nativecode.global list
val module_of_library : compiled_library -> Declarations.module_body
val univs_of_library : compiled_library -> Univ.ContextSet.t
val start_library : Names.DirPath.t -> Names.ModPath.t safe_transformer
val export : ?⁠except:Future.UUIDSet.t -> output_native_objects:bool -> safe_environment -> Names.DirPath.t -> Names.ModPath.t * compiled_library * native_library
val import : compiled_library -> Univ.ContextSet.t -> vodigest -> Names.ModPath.t safe_transformer
Safe typing judgments
type judgment
val j_val : judgment -> Constr.constr
val j_type : judgment -> Constr.constr
val typing : safe_environment -> Constr.constr -> judgment

The safe typing of a term returns a typing judgment.

Queries
val exists_objlabel : Names.Label.t -> safe_environment -> bool
val delta_of_senv : safe_environment -> Mod_subst.delta_resolver * Mod_subst.delta_resolver
val constant_of_delta_kn_senv : safe_environment -> Names.KerName.t -> Names.Constant.t
val mind_of_delta_kn_senv : safe_environment -> Names.KerName.t -> Names.MutInd.t
Retroknowledge / Native compiler
val register_inline : Names.Constant.t -> safe_transformer0
val register_inductive : Names.inductive -> 'a CPrimitives.prim_ind -> safe_transformer0
val set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0