OpaqueproofThis module implements the handling of opaque proof terms. Opaque proof terms are special since:
opaque proof terms holds an index into an opaque table.type 'a delayed_universes = | PrivateMonomorphic of 'a | |
| PrivatePolymorphic of Univ.ContextSet.t | (* local constraints *) |
val empty_opaquetab : opaquetabval create : Names.DirPath.t -> opaquetab -> opaque * opaquetabtype opaque_proofterm = Constr.t * unit delayed_universesmodule HandleMap : CSig.MapS with type key = opaque_handleOpaque 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 subst_opaque : Mod_subst.substitution -> opaque -> opaqueval discharge_opaque : Cooking.cooking_info -> opaque -> opaqueval repr_handle : opaque_handle -> intval mem_handle : opaque_handle -> opaquetab -> boolval repr : opaque -> Mod_subst.substitution list * Cooking.cooking_info list * Names.DirPath.t * opaque_handle