Module `Safe_typing`

type vodigest = | Dvo_or_vi of Stdlib.Digest.t | Dvivo of Stdlib.Digest.t * Stdlib.Digest.t

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

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 : ?⁠typing_flags:Declarations.typing_flags -> 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 : ?⁠typing_flags:Declarations.typing_flags -> 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

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

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

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 * Nativelib.native_library
val import : compiled_library -> Univ.ContextSet.t -> vodigest -> Names.ModPath.t safe_transformer

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.

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

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