You are viewing the staging branch of the website @ 58d46ed, 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 (using coq-platform supplied version of Flocq)

Install

Dune Dependency

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

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: 06 May 2020

Dependencies (5)

ocaml >= "4.05.0"
menhir >= "20190626" & < "20200123"
coq-menhirlib >= "20190626" & < "20200123"
coq-flocq >= "3.2.1"
coq >= "8.7.0" & < "8.12"

Dev Dependencies

None

Used by (1)

coq-vst = "2.6"

Conflicts

None

On This Page

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