Module Opaqueproof

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

local constraints

type opaquetab
type opaque
val empty_opaquetab : opaquetab
val create : Names.DirPath.t -> opaquetab -> opaque * opaquetab
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 -> opaque -> opaque
val discharge_opaque : Cooking.cooking_info -> opaque -> opaque
val repr_handle : opaque_handle -> int
val mem_handle : opaque_handle -> opaquetab -> bool
val repr : opaque -> Mod_subst.substitution list * Cooking.cooking_info list * Names.DirPath.t * opaque_handle