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

    Number of surrounding bound universes + local constraints

    *)
type opaquetab
type 'cooking_info opaque
val empty_opaquetab : opaquetab
val create : Names.DirPath.t -> opaquetab -> 'c opaque * opaquetab

Create a fresh handle in the table.

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