package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 'a const_entry_body = 'a Entries.proof_output Future.computation
val declare_defined_opaque : ?feedback_id:Stateid.t -> Opaqueproof.opaque_handle -> Safe_typing.private_constants const_entry_body -> unit
val declare_private_opaque : Safe_typing.exported_opaque -> unit
type opaque_disk
val get_current_opaque : Opaqueproof.opaque_handle -> Opaqueproof.opaque_proofterm option
val get_current_constraints : Opaqueproof.opaque_handle -> Univ.ContextSet.t option
module Summary : sig ... end