A Coq plugin for simpler proofs by reflection or OCaml certificates.
http://cybele.gforge.inria.fr/
Make sure that you added the Coq repository:
opam repo add coq-released https://coq.inria.fr/opam/released
and run:
opam install coq-cybele
This plugin works with the 8.5 branch of Coq.
Before anything else, make sure that all the utilities of Coq are in your path. Compile by typing:
./configure.sh
make
Finally, install your plugin:
make install
(as root if necessary).
Go to test-suite/. You can try out each example doing a:
./configure.sh
make