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
val get_opaque_disk :
Opaqueproof.opaque_handle ->
opaque_disk ->
Opaqueproof.opaque_proofterm option
val set_opaque_disk :
Opaqueproof.opaque_handle ->
Opaqueproof.opaque_proofterm ->
opaque_disk ->
unit
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