Module Opaqueproof

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

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) option
type indirect_accessor = {
access_proof : Names.DirPath.t -> int -> opaque_proofterm;
access_discharge : cooking_info list -> (Constr.t * unit delayed_universes) -> Constr.t * unit delayed_universes;
}

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 -> Constr.constr * unit delayed_universes

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
val dump : ?⁠except:Future.UUIDSet.t -> opaquetab -> opaque_proofterm array * int Future.UUIDMap.t