Module Safe_typing
Safe environments
val empty_environment : safe_environmentval is_initial : safe_environment -> boolval env_of_safe_env : safe_environment -> Environ.envval sections_of_safe_env : safe_environment -> section_data Section.t
type safe_transformer0= safe_environment -> safe_environmenttype 'a safe_transformer= safe_environment -> 'a * safe_environment
Stm machinery
val empty_private_constants : private_constantsval concat_private : private_constants -> private_constants -> private_constantsconcat_private e1 e2adds the constants ofe1toe2, i.e. constants ine1must be more recent than those ofe2.
val mk_pure_proof : Constr.constr -> private_constants Entries.proof_outputval inline_private_constants : Environ.env -> private_constants Entries.proof_output -> Constr.constr Univ.in_universe_context_setval push_private_constants : Environ.env -> private_constants -> Environ.envPush the constants in the environment if not already there.
val universes_of_private : private_constants -> Univ.ContextSet.tval is_curmod_library : safe_environment -> boolval join_safe_environment : ?except:Future.UUIDSet.t -> safe_environment -> safe_environmentval is_joined_environment : safe_environment -> boolEnriching a safe environment
type global_declaration=|ConstantEntry : Entries.constant_entry -> global_declaration|OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declarationtype side_effect_declaration=|DefinitionEff : Entries.definition_entry -> side_effect_declaration|OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declarationtype exported_private_constant= Names.Constant.t
val export_private_constants : private_constants Entries.proof_output -> (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformerval add_constant : Names.Label.t -> global_declaration -> Names.Constant.t safe_transformerreturns the main constant
val add_private_constant : Names.Label.t -> side_effect_declaration -> (Names.Constant.t * private_constants) safe_transformerSimilar 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_transformerval 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_transformer0val add_constraints : Univ.Constraint.t -> safe_transformer0val set_engagement : Declarations.engagement -> safe_transformer0Setting the type theory flavor
val set_indices_matter : bool -> safe_transformer0val set_typing_flags : Declarations.typing_flags -> safe_transformer0val set_check_guarded : bool -> safe_transformer0val set_check_positive : bool -> safe_transformer0val set_check_universes : bool -> safe_transformer0val set_VM : bool -> safe_transformer0val set_native_compiler : bool -> safe_transformer0val make_sprop_cumulative : safe_transformer0val set_allow_sprop : bool -> safe_transformer0val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
Interactive section functions
val open_section : safe_transformer0val close_section : safe_transformer0val sections_are_opened : safe_environment -> bool
val push_named_assum : (Names.Id.t * Constr.types) -> safe_transformer0val push_named_def : (Names.Id.t * Entries.section_def_entry) -> safe_transformer0val push_section_context : (Names.Name.t array * Univ.UContext.t) -> safe_transformer0Add local universes to a polymorphic section
Interactive module functions
val start_module : Names.Label.t -> Names.ModPath.t safe_transformerval start_modtype : Names.Label.t -> Names.ModPath.t safe_transformerval add_module_parameter : Names.MBId.t -> Entries.module_struct_entry -> Declarations.inline -> Mod_subst.delta_resolver safe_transformerval allow_delayed_constants : bool Stdlib.refTraditional 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_transformerval end_modtype : Names.Label.t -> (Names.ModPath.t * Names.MBId.t list) safe_transformerval add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver safe_transformerval current_modpath : safe_environment -> Names.ModPath.tval current_dirpath : safe_environment -> Names.DirPath.t
Libraries : loading and saving compilation units
type compiled_librarytype native_library= Nativecode.global list
val module_of_library : compiled_library -> Declarations.module_bodyval start_library : Names.DirPath.t -> Names.ModPath.t safe_transformerval export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> safe_environment -> Names.DirPath.t -> Names.ModPath.t * compiled_library * native_libraryval import : compiled_library -> Univ.ContextSet.t -> vodigest -> Names.ModPath.t safe_transformer
Safe typing judgments
val j_val : judgment -> Constr.constrval j_type : judgment -> Constr.constrval typing : safe_environment -> Constr.constr -> judgmentThe safe typing of a term returns a typing judgment.
Queries
val exists_objlabel : Names.Label.t -> safe_environment -> boolval delta_of_senv : safe_environment -> Mod_subst.delta_resolver * Mod_subst.delta_resolverval constant_of_delta_kn_senv : safe_environment -> Names.KerName.t -> Names.Constant.tval mind_of_delta_kn_senv : safe_environment -> Names.KerName.t -> Names.MutInd.t
Retroknowledge / Native compiler
val register_inline : Names.Constant.t -> safe_transformer0val register_inductive : Names.inductive -> 'a CPrimitives.prim_ind -> safe_transformer0val set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0