Home

Description

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

To do

• README
• Documentation of the makefile (and how to use coq_makefile)
• Documentation of how to install a plugin
• 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 ?
• Better hash function ?