package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type vodigest =
  1. | Dvo_or_vi of Digest.t
  2. | 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_constants
val side_effects_of_private_constants : private_constants -> Entries.side_eff list
val empty_private_constants : private_constants
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 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
type !'a effect_entry =
  1. | EffectEntry : private_constants effect_entry
  2. | PureEntry : unit effect_entry
type global_declaration =
  1. | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration
  2. | 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 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 allow_delayed_constants : bool ref
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
type judgment
val j_val : judgment -> Constr.constr
val j_type : judgment -> Constr.constr
val exists_objlabel : Names.Label.t -> safe_environment -> bool
val retroknowledge : (Retroknowledge.retroknowledge -> 'a) -> safe_environment -> 'a
  • deprecated Use the projection of Environ.env
val register_inline : Names.Constant.t -> safe_transformer0