Module `Opaqueproof`Source

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 =

| PrivateMonomorphic of 'a
| PrivatePolymorphic of int * Univ.ContextSet.t
(*
Number of surrounding bound universes + local constraints
*)

type proofterm =
  (Constr.constr * Univ.ContextSet.t delayed_universes) Future.computation

Sourcetype opaquetab

Sourcetype opaque

Sourceval empty_opaquetab : opaquetab

Sourceval create : Names.DirPath.t -> proofterm -> opaquetab -> opaque * opaquetab

From a proofterm to some opaque.

Source

type work_list =
  (Univ.Instance.t * Names.Id.t array) Names.Cmap.t
  * (Univ.Instance.t * Names.Id.t array) Names.Mindmap.t

Sourcetype cooking_info = {

modlist : work_list;
abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t;

}

Sourcetype opaque_proofterm = Constr.t * unit delayed_universes

Sourcetype opaque_handle

Sourcetype indirect_accessor = {

access_proof : Names.DirPath.t -> opaque_handle -> opaque_proofterm option;
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.

Sourceval force_proof : indirect_accessor -> opaquetab -> opaque -> opaque_proofterm

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

Source

val force_constraints : 
  indirect_accessor ->
  opaquetab ->
  opaque ->
  Univ.ContextSet.t

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

Source

val dump : 
  ?except:Future.UUIDSet.t ->
  opaquetab ->
  opaque_disk * opaque_handle Future.UUIDMap.t

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

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Opaqueproof`Source

Serialization

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module OpaqueproofSource

Serialization

Module `Opaqueproof`Source