coq-tutorial-ml-tactics
coq-tutorial-ml-tactics copied to clipboard
braibant
A tutorial on how to write OCaml tactics for the Coq proof assistant
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. The project needs coq8.5(pl2).
INSTRUCTIONS
- Build the makefile with:
coq_makefile -f arguments.txt -o Makefile
- run "make"
FILES DESCRIPTION
arguments.txt : the pre-makefile that is fed to coq_makefile (coq_makefile -f arguments.txt -o Makefile) src/lib_coq.ml{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.
braibant