package coq-metacoq-template-pcuic
Translations between Template Coq and PCUIC and proofs of correctness
Install
Dune Dependency
Authors
Maintainers
Sources
v1.2-8.16.tar.gz
sha512=1fc976740f2ff5a6c4137cf4722e09cae5765d0d71f55e6a020883218396856558a6534aa7d2bd192b60778427edbbc2f096a0e738e95551808702613edbbb31
Description
Published: 22 Apr 2023
Dependencies (2)
-
coq-metacoq-pcuic
= version
-
coq-metacoq-template
= version
Dev Dependencies
None
Used by (4)
-
coq-metacoq-erasure
= "1.2+8.16"
-
coq-metacoq-erasure-plugin
< "1.2+8.17"
-
coq-metacoq-quotation
< "1.2+8.17"
-
coq-metacoq-safechecker-plugin
< "1.2+8.17"
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)" x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)">
On This Page