Skip to content


Subversion checkout URL

You can clone with
Download ZIP
A tutorial on how to write OCaml tactics for the Coq proof assistant
OCaml Verilog
branch: master

Hashing modulo eq_constr & hash_constr

latest commit ca593086a0
Pierre Boutillier authored


An example of Coq plugin that defines a reification tactic. 

The files should be self-documented, even though we may manage to build a pdf that summarizes every interesting point. At the moment, the project needs coq trunk, in order to build the Makefile (coq_makefile ws evely patched recently). 


arguments.txt : the pre-makefile that is fed to coq_makefile (coq_makefile -f arguments.txt -o Makefile)
src/{i} : an interface with Coq, where we define some handlers for Coq's API and constructs. 
src/plugin.ml4 : the actual plugin that defines a reification tactic for a very simple subset of terms on nat
src/Theory.v : reification primer
test-suite/example.v : an example of usage of the tactic we defined in src/plugin.ml4. 

Something went wrong with that request. Please try again.