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_constant
type private_constants
type private_constant_role =
  1. | Subproof
  2. | Schema of Names.inductive * string
val side_effects_of_private_constants : private_constants -> Entries.side_effect list
val empty_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 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 * 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 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 Pervasives.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
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