Module `Safe_typing`

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

val side_effects_of_private_constants : private_constants -> Entries.side_eff list: Return the list of individual side-effects in the order of their creation.

val empty_private_constants : private_constants
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 private_con_of_con : safe_environment -> Names.Constant.t -> private_constants
val private_con_of_scheme : kind:string -> safe_environment -> (Names.inductive * Names.Constant.t) list -> private_constants
val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
val inline_private_constants_in_constr : Environ.env -> Constr.constr -> private_constants -> Constr.constr
val inline_private_constants_in_definition_entry : Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
val universes_of_private : private_constants -> Univ.ContextSet.t list
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

val push_named_assum : (Names.Id.t * Constr.types * bool) Univ.in_universe_context_set -> safe_transformer0
val push_named_def : (Names.Id.t * Entries.section_def_entry) -> safe_transformer0: Returns the full universe context necessary to typecheck the definition (futures are forced)

type 'a effect_entry = | EffectEntry : private_constants effect_entry | PureEntry : unit effect_entry
type global_declaration = | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration | GlobalRecipe of Cooking.recipe
type exported_private_constant = Names.Constant.t * Entries.side_effect_role

val export_private_constants : in_section:bool -> private_constants Entries.definition_entry -> (unit Entries.definition_entry * exported_private_constant list) safe_transformer
val add_constant : in_section:bool -> Names.Label.t -> global_declaration -> Names.Constant.t safe_transformer: returns the main constant plus a list of auxiliary constants (empty unless one requires the side effects to be exported)

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 : 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_VM : bool -> safe_transformer0
val set_native_compiler : bool -> safe_transformer0
val make_sprop_cumulative : safe_transformer0
val set_allow_sprop : bool -> safe_transformer0
val check_engagement : Environ.env -> Declarations.set_predicativity -> unit

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 get_library_native_symbols : safe_environment -> Names.DirPath.t -> Nativecode.symbols
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

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 -> CPrimitives.prim_ind -> safe_transformer0
val set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0