Module Opaqueproof

type 'a delayed_universes =
| PrivateMonomorphic of 'a
| PrivatePolymorphic of int * Univ.ContextSet.t

Number of surrounding bound universes + local constraints

type proofterm = (Constr.constr * Univ.ContextSet.t delayed_universes) Future.computation
type opaquetab
type opaque
val empty_opaquetab : opaquetab
val create : Names.DirPath.t -> proofterm -> opaquetab -> opaque * opaquetab

From a proofterm to some opaque.

type work_list = (Univ.Instance.t * Names.Id.t array) Names.Cmap.t * (Univ.Instance.t * Names.Id.t array) Names.Mindmap.t
type cooking_info = {
modlist : work_list;
abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t;
}
type opaque_proofterm = Constr.t * unit delayed_universes
type opaque_handle
type indirect_accessor = {
access_proof : Names.DirPath.t -> opaque_handle -> opaque_proofterm option;
access_discharge : cooking_info list -> opaque_proofterm -> opaque_proofterm;
}

Opaque terms are indexed by their library dirpath and an integer index. The two functions above activate this indirect storage, by telling how to retrieve terms.

val force_proof : indirect_accessor -> opaquetab -> opaque -> opaque_proofterm

From a opaque back to a constr. This might use the indirect opaque accessor given as an argument.

val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t
val subst_opaque : Mod_subst.substitution -> opaque -> opaque
val discharge_opaque : cooking_info -> opaque -> opaque
val join_opaque : ?⁠except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
Serialization
type opaque_disk
val dump : ?⁠except:Future.UUIDSet.t -> opaquetab -> opaque_disk * opaque_handle Future.UUIDMap.t
val get_opaque_disk : opaque_handle -> opaque_disk -> opaque_proofterm option
val set_opaque_disk : opaque_handle -> opaque_proofterm -> opaque_disk -> unit
val repr_handle : opaque_handle -> int

Only used for pretty-printing