package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
doc/coq-core.kernel/Opaqueproof/index.html
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.
Source
type 'a delayed_universes =
| PrivateMonomorphic of 'a
| PrivatePolymorphic of Univ.ContextSet.t
(*local constraints
*)
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.
Source
val repr :
opaque ->
Mod_subst.substitution list
* Cooking.cooking_info list
* Names.DirPath.t
* opaque_handle
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>