Module `Opaqueproof`

This module implements the handling of opaque proof terms. Opaque proof terms are special since:

they can be lazily computed and substituted
they are stored in an optionally loaded segment of .vo files An opaque proof terms holds the real data until fully discharged. In this case it is called direct. When it is turn_indirect the data is relocated to an opaque table and the opaque is turned into an index.

type proofterm = (Constr.constr * Univ.ContextSet.t) Future.computation
type opaquetab
type opaque

val empty_opaquetab : opaquetab
val create : proofterm -> opaque: From a proofterm to some opaque.

val turn_indirect : Names.DirPath.t -> opaque -> opaquetab -> opaque * opaquetab: Turn a direct opaque into an indirect one. It is your responsibility to hashcons the inner term beforehand. The integer is an hint of the maximum id used so far

val force_proof : opaquetab -> opaque -> Constr.constr: From a opaque back to a constr. This might use the indirect opaque accessor configured below.

val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
val get_proof : opaquetab -> opaque -> Constr.constr Future.computation
val get_constraints : opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
val subst_opaque : Mod_subst.substitution -> opaque -> opaque
val iter_direct_opaque : (Constr.constr -> unit) -> opaque -> 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; }

val discharge_direct_opaque : cook_constr:(Constr.constr -> Constr.constr) -> cooking_info -> opaque -> opaque
val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option
val join_opaque : opaquetab -> opaque -> unit
val dump : opaquetab -> Constr.t Future.computation array * Univ.ContextSet.t Future.computation array * cooking_info list array * int Future.UUIDMap.t

val set_indirect_opaque_accessor : (Names.DirPath.t -> int -> Constr.constr Future.computation) -> unit
val set_indirect_univ_accessor : (Names.DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit