Module `Opaqueproof`

type 'a delayed_universes = | PrivateMonomorphic of 'a | PrivatePolymorphic of int * Univ.ContextSet.t Number of surrounding bound universes + local constraints
type opaquetab
type 'cooking_info opaque

val empty_opaquetab : opaquetab
val create : Names.DirPath.t -> opaquetab -> 'c opaque * opaquetab: Create a fresh handle in the table.

type opaque_proofterm = Constr.t * unit delayed_universes
type opaque_handle

module HandleMap : CSig.MapS with type key = opaque_handle

val subst_opaque : Mod_subst.substitution -> 'c opaque -> 'c opaque
val discharge_opaque : 'cooking_info -> 'cooking_info opaque -> 'cooking_info opaque
val repr_handle : opaque_handle -> int
val mem_handle : opaque_handle -> opaquetab -> bool
val repr : 'c opaque -> Mod_subst.substitution list * 'c list * Names.DirPath.t * opaque_handle