coq 8.8.1 · OCaml Package

type vodigest =

| Dvo_or_vi of Digest.t
| Dvivo of Digest.t * Digest.t

val digest_match : actual:vodigest -> required:vodigest -> bool

type safe_environment

val empty_environment : safe_environment

val is_initial : safe_environment -> bool

val env_of_safe_env : safe_environment -> Environ.env

type safe_transformer0 = safe_environment -> safe_environment

type !'a safe_transformer = safe_environment -> 'a * safe_environment

type private_constant

type private_constants

type private_constant_role =

| Subproof
| Schema of Names.inductive * string

val side_effects_of_private_constants : 
  private_constants ->
  Entries.side_effect list

val empty_private_constants : private_constants

val add_private : private_constant -> private_constants -> private_constants

val concat_private : 
  private_constants ->
  private_constants ->
  private_constants

val private_con_of_con : 
  safe_environment ->
  Names.Constant.t ->
  private_constant

val private_con_of_scheme : 
  kind:string ->
  safe_environment ->
  (Names.inductive * Names.Constant.t) list ->
  private_constant

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

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

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 * private_constant_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 : 
  Names.DirPath.t ->
  Names.Label.t ->
  global_declaration ->
  Names.Constant.t safe_transformer

val add_mind : 
  Names.DirPath.t ->
  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 push_context : bool -> Univ.UContext.t -> safe_transformer0

val add_constraints : Univ.Constraint.t -> safe_transformer0

val set_engagement : Declarations.engagement -> safe_transformer0

val set_typing_flags : Declarations.typing_flags -> safe_transformer0

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 ref

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

type compiled_library

type native_library = Nativecode.global list

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 ->
  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

type judgment

val j_val : judgment -> Constr.constr

val j_type : judgment -> Constr.constr

val typing : safe_environment -> Constr.constr -> 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 retroknowledge : 
  (Retroknowledge.retroknowledge -> 'a) ->
  safe_environment ->
  'a

val register : 
  Retroknowledge.field ->
  Retroknowledge.entry ->
  Constr.constr ->
  safe_transformer0

val register_inline : Names.Constant.t -> safe_transformer0

val set_strategy : 
  safe_environment ->
  Names.Constant.t Names.tableKey ->
  Conv_oracle.level ->
  safe_environment

package coq