Module OpaqueproofSource

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

Sourcetype 'a delayed_universes =
  1. | PrivateMonomorphic of 'a
  2. | PrivatePolymorphic of int * Univ.ContextSet.t
    (*

    Number of surrounding bound universes + local constraints

    *)
Sourcetype opaquetab
Sourcetype opaque
Sourceval empty_opaquetab : opaquetab

From a proofterm to some opaque.

Sourcetype cooking_info = {
  1. modlist : work_list;
  2. abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t;
}
Sourcetype opaque_proofterm = Constr.t * unit delayed_universes
Sourcetype opaque_handle
Sourcetype indirect_accessor = {
  1. access_proof : Names.DirPath.t -> opaque_handle -> opaque_proofterm option;
  2. access_discharge : cooking_info list -> opaque_proofterm -> opaque_proofterm;
}

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.

From a opaque back to a constr. This might use the indirect opaque accessor given as an argument.

Sourceval subst_opaque : Mod_subst.substitution -> opaque -> opaque
Sourceval discharge_opaque : cooking_info -> opaque -> opaque
Sourceval join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
Serialization
Sourcetype opaque_disk
Sourceval get_opaque_disk : opaque_handle -> opaque_disk -> opaque_proofterm option
Sourceval set_opaque_disk : opaque_handle -> opaque_proofterm -> opaque_disk -> unit
Sourceval repr_handle : opaque_handle -> int

Only used for pretty-printing