diff options
author | Stephane Glondu <steph@glondu.net> | 2010-11-29 23:30:48 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-11-29 23:30:48 +0100 |
commit | 1aa8b6f6a876af22f538c869f022bc4ca5986b40 (patch) | |
tree | 037f0286a86b2bcee9bfa08f00112005a71e0e18 /README.txt |
Imported Upstream version 0.1-r13244upstream/0.1-r13244
Diffstat (limited to 'README.txt')
-rw-r--r-- | README.txt | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/README.txt b/README.txt new file mode 100644 index 0000000..ad3b5c9 --- /dev/null +++ b/README.txt @@ -0,0 +1,65 @@ + + aac_tactics + =========== + + Thomas Braibant & Damien Pous + +Laboratoire d'Informatique de Grenoble (UMR 5217), INRIA, CNRS, France + +Webpage of the project: http://sardes.inrialpes.fr/~braibant/aac_tactics/ + + +FOREWORD +======== + +This plugin provides tactics for rewriting universally quantified +equations, modulo associativity and commutativity of some operators. + +INSTALL +======= + +- run [./make_makefile] in the top-level directory to generate a Makefile +- run [make world] to build the plugin and the documentation + +This should work with Coq v8.3 `beta' : -r 13027, -r 13060 and hopefully the +following ones. + +To be able to import the plugin from anywhere, add the following to +your ~/.coqrc + +Add Rec LoadPath "path_to_aac_tactics". +Add ML Path "path_to_aac_tactics". + + +DOCUMENTATION +============= + +Please refer to Tutorial.v for a succint introduction on how to use +this plugin. + +To understand the inner-working of the tactic, please refer to the +.mli files as the main source of information on each .ml +file. Alternatively, [make world] generates ocamldoc/coqdoc +documentation in directories doc/ and html/, respectively. + +File Instances.v defines several instances for frequent use-cases of +this plugin, that should allow you to use it out-of-the-shelf. Namely, +we have instances for: + +- Peano naturals (Import Instances.Peano) +- Z binary numbers (Import Instances.Z) +- Rationnal numbers (Import Instances.Q) +- Prop (Import Instances.Prop_ops) +- Booleans (Import Instances.Bool) +- Relations (Import Instances.Relations) +- All of the above (Import Instances.All) + + +ACKNOWLEDGEMENTS +================ + +We are grateful to Evelyne Contejean, Hugo Herbelin, Assia Mahboubi +and Matthieu Sozeau for highly instructive discussions. + +This plugin took inspiration from the plugin tutorial "constructors", +distributed under the LGPL 2.1, copyrighted by Matthieu Sozeau |