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 option
val structure_body_of_safe_env : safe_environment -> Declarations.structure_body
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 is_empty_private_constants : private_constants -> bool
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 export_private_constants : private_constants -> exported_private_constant list safe_transformer
val push_context_set : strict: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 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
val module_of_library : compiled_library -> Declarations.module_body
val univs_of_library : compiled_library -> Univ.ContextSet.t
val export : ?except:Future.UUIDSet.t -> output_native_objects:bool -> safe_environment -> Names.DirPath.t -> Names.ModPath.t * compiled_library * Nativelib.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