You are viewing the staging branch of the website @ 884bba1, not the live version.

package coq-metacoq-template-pcuic

Translations between Template Coq and PCUIC and proofs of correctness

Install

Dune Dependency

metacoq.github.io Edit opam file Versions (12)

Authors

Maintainers

M

matthieu.sozeau@inria.fr

Sources

v1.3.4-8.20.tar.gz

sha512=fb3997e2e07e9c33c293aabcc06b8e69785a9c2ebdcd4d48f77e1eb09698da6ed1770127022843f89322cf8f78289acd67c860e1a2d9186d5703191ccd088429

Description

Published: 28 Jan 2025

Dependencies (2)

coq-metacoq-pcuic = version
coq-metacoq-template = version

Dev Dependencies

None

Used by (6)

coq-elm-extraction
coq-metacoq-erasure >= "1.3.4+8.20"
coq-metacoq-erasure-plugin >= "1.3.4+8.20"
coq-metacoq-quotation >= "1.3.4+8.20"
coq-metacoq-safechecker-plugin >= "1.3.4+8.20"
coq-rust-extraction

Conflicts

None

On This Page

Description
Dependencies (2)
Dev Dependencies
Used by (6)
Conflicts