Popular repositories

1. mirror-core Public

   A framework for extensible, reflective decision procedures.

   Coq 19 5

2. coq-printf Public

   Implementation of sprintf for Coq

   Coq 18 2

3. coq-interaction-trees Public

   Co-inductive interaction trees provide a way to represent (potentially) non-terminating programs with I/O behavior.

   Coq 17 1

4. template-coq Public

   Forked from MetaCoq/metacoq

   Reflection library for Coq

   OCaml 12

5. coq-ltac-iter Public

   Access hint databases from tactics.

   Coq 12 3

6. coq-smt-check Public

   Invoke SMT solvers from Coq to check obligations

   OCaml 9 3