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 Univ.ContextSet.t(*

local constraints

type opaquetab
type opaque
val empty_opaquetab : opaquetab
type opaque_proofterm = Constr.t * unit delayed_universes
type opaque_handle
module HandleMap : CSig.MapS with type key = opaque_handle

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 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