Home

Description

This is a plugin example, describing how to build reification tactics in ML.

Installation

At the moment, it requires to use the trunk version of Coq (that will become 8.4). The rationale behind this is that coq_makefile from version 8.3 built Makefile that required a lot of patching using a (huge) shell script. This has been addressed in July in the trunk (and some nifty improvements have been made).

To build the project do:

coq_makefile -f arguments.txt -o Makefile  
make  

To do

• README
• Documentation of the makefile (and how to use coq_makefile)
• Documentation of how to install a plugin (in the coq/plugin directory)
• License
• Discuss the Mltop.add_known_module
• What is the structure that Coq plugins should have ?
• src/ for ml files, theories/ for Coq files, test-suite/ for examples, and regression tests ?
• src/ for ml files and Coq files, test-suite/ for examples, and regression tests ?
• something else ?
• is it important ?