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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct