Module Opaques

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
val dump : ?except:Future.UUIDSet.t -> unit -> opaque_disk * Opaqueproof.opaque_handle Future.UUIDMap.t
module Summary : sig ... end