Find file
Fetching contributors…
Cannot retrieve contributors at this time
40 lines (29 sloc) 1.3 KB
Reify: an efficient reification framework.
Copyright 2010 Matthieu Sozeau <>
This archive contains a plugin for reification of
arbitrary expressions in Coq. It uses an efficient [varmap]
structure to hold the uninterpreted expressions and allows to
declare reification clauses as simple type class instances to
customize the reification.
The archive has 3 subdirectories:
src/ contains the code of the tactics in and
a support file for building the plugin.
theories/ contains support Coq files for the plugin.
Dynamic.v is used to share terms between Coq and ML code.
Reify.v declares the plugin on the Coq side and defines
supporting definitions.
test-suite/ has a few example uses of the plugin.
First, you should have coqc, ocamlc and make in your path.
Then simply do:
# coq_makefile -f Make -o Makefile
To generate a makefile from the description in Make, then [make].
This will consecutively build the plugin, the supporting
theories and the test-suite file.
You can then either [make install] the plugin or leave it in its
current directory. To be able to import it from anywhere in Coq,
simply add the following to ~/.coqrc:
Add Rec LoadPath "path_to_plugin/theories" as Reify.
Add ML Path "path_to_plugin/src".