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
type section_data
val empty_environment : safe_environment
val is_initial : safe_environment -> bool
val env_of_safe_env : safe_environment -> Environ.env
val sections_of_safe_env : safe_environment -> section_data Section.t
type safe_transformer0 = safe_environment -> safe_environment
type !'a safe_transformer = safe_environment -> 'a * safe_environment
type private_constants
val empty_private_constants : private_constants
val push_private_constants : Environ.env -> private_constants -> Environ.env
val universes_of_private : private_constants -> Univ.ContextSet.t
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 side_effect_declaration =
  1. | DefinitionEff : Entries.definition_entry -> side_effect_declaration
  2. | OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration
type exported_private_constant = Names.Constant.t
val push_context_set : bool -> Univ.ContextSet.t -> safe_transformer0
val add_constraints : Univ.Constraint.t -> safe_transformer0
val set_indices_matter : bool -> safe_transformer0
val set_share_reduction : bool -> safe_transformer0
val set_check_guarded : bool -> safe_transformer0
val set_check_positive : bool -> safe_transformer0
val set_check_universes : bool -> safe_transformer0
val set_VM : bool -> safe_transformer0
val set_native_compiler : bool -> safe_transformer0
val make_sprop_cumulative : safe_transformer0
val set_allow_sprop : bool -> safe_transformer0
val check_engagement : Environ.env -> Declarations.set_predicativity -> unit
val open_section : safe_transformer0
val close_section : safe_transformer0
val sections_are_opened : safe_environment -> bool
val push_named_assum : (Names.Id.t * Constr.types) -> safe_transformer0
val push_section_context : (Names.Name.t array * Univ.UContext.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 module_of_library : compiled_library -> Declarations.module_body
val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> safe_environment -> Names.DirPath.t -> Names.ModPath.t * compiled_library * native_library
type judgment
val j_val : judgment -> Constr.constr
val j_type : judgment -> Constr.constr
val exists_objlabel : Names.Label.t -> safe_environment -> bool
val constant_of_delta_kn_senv : safe_environment -> Names.KerName.t -> Names.Constant.t
val mind_of_delta_kn_senv : safe_environment -> Names.KerName.t -> Names.MutInd.t
val register_inline : Names.Constant.t -> safe_transformer0
val register_inductive : Names.inductive -> 'a CPrimitives.prim_ind -> 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