package coq-verified-extraction

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

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

  1. Y
    Yannick Forster
  2. M
    Matthieu Sozeau
  3. N
    Nicolas Tabareau

Maintainers

  1. M
    Matthieu Sozeau <matthieu.sozeau@inria.fr

Sources

coq-verified-extraction-0.9.2-8.19.tar.gz
sha512=ecd392ee3778fc50e7bf77b6efe81dc4b48232efd7aceb5d2ba09a44accdda6a181042d38483bed9793cfced4bc3c671c2c5bd1296fbb6bb244219d69bf685c9

Description

Published: 23 Jul 2024

Dependencies (7)

  1. coq-metacoq-erasure-plugin >= "1.3.2+8.19"
  2. coq-metacoq-erasure >= "1.3.2+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