package coq-verified-extraction

  1. Overview
  2. Homepage
A Verified Extraction from Gallina to OCaml, written in Gallina

Install

Dune Dependency

Authors

Maintainers

Sources

coq-verified-extraction-0.9.1-8.19.tar.gz
sha512=c1c99473acc9fdca362b82c0b71d1cc0a00a91f7471e98b3a3ea177295f7b4acab8cda04520762856e9ac9465fbb3138b9b905a46a66e693c8d8c47a10e739c2

Description

Published: 12 Jul 2024

Dependencies (7)

  1. coq-metacoq-erasure-plugin >= "1.3.1+8.19"
  2. coq-metacoq-erasure >= "1.3.1+8.19"
  3. coq-equations = "1.3+8.19"
  4. coq-ceres >= "0.4.1"
  5. coq >= "8.19" & < "8.20~"
  6. malfunction >= "0.6"
  7. ocaml >= "4.13"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover