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

package coq-compcert

You can search for identifiers within the package.

in-package search v0.2.0

The CompCert C compiler (only open source files + using coq-platform)

Install

Dune Dependency

compcert.inria.fr Edit opam file Versions (30)

Authors

Xavier Leroy

Maintainers

J

Jacques-Henri Jourdan <jacques-Henri.jourdan@normalesup.org>

Sources

sha256=ceee1b2ed6c2576cb66eb7a0f2669dcf85e65c0fc68385f0781b0ca4edb87eb0

Description

Tags

category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:C keyword:compiler logpath:compcert date:2020-04-29

Published: 28 Jul 2020

Dependencies (5)

ocaml >= "4.05.0"
menhir >= "20190626" & <= "20210310"
coq-menhirlib >= "20190626" & <= "20210310"
coq-flocq >= "3.2.1" & < "4~"
coq >= "8.12" & < "8.13"

Dev Dependencies

None

Used by (1)

coq-vst = "2.6"

Conflicts

None

On This Page

Description
Dependencies (5)
Dev Dependencies
Used by (1)
Conflicts