package coq

  1. Overview
  2. Docs
On This Page
  1. Serialization
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.14.0.tar.gz
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c

doc/coq-core.kernel/Opaqueproof/index.html

Module OpaqueproofSource

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