package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

  • they can be lazily computed and substituted
  • they are stored in an optionally loaded segment of .vo files An opaque proof terms holds an index into an opaque table.
type 'a delayed_universes =
  1. | PrivateMonomorphic of 'a
  2. | 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