Reification for Coq
OCaml Verilog
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.


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".