diff options
author | Nicolas Braud-Santoni <nicolas@braud-santoni.eu> | 2016-07-23 16:22:24 -0400 |
---|---|---|
committer | Nicolas Braud-Santoni <nicolas@braud-santoni.eu> | 2016-07-23 16:22:24 -0400 |
commit | a3a7c528787411373bb857af4b51f3003f9fcc2b (patch) | |
tree | 364a89e76f79bbf82818401a2e1fc2d37f7f84cc /README | |
parent | 2614d6df738735538ea381e44bad1279269676c1 (diff) | |
parent | 17564e4922acda6b72bf39de7a8c23ed0c0178f6 (diff) |
Merge tag 'upstream/8.5.1'
Upstream version 8.5.1
Diffstat (limited to 'README')
-rw-r--r-- | README | 55 |
1 files changed, 55 insertions, 0 deletions
@@ -0,0 +1,55 @@ + + aac_tactics + =========== + + Thomas Braibant & Damien Pous + +Laboratoire d'Informatique de Grenoble (UMR 5217), INRIA, CNRS, France + + +FOREWORD +======== + +This plugin provides tactics for rewriting universally quantified +equations, modulo associativity and commutativity of some operators. + +INSTALLATION +============ + +opam repo add coq-released https://coq.inria.fr/opam/released +opam install coq-aac-tactics + +DOCUMENTATION +============= + +Please refer to Tutorial.v for a succinct 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) +- N binary numbers (Import Instances.N) +- P binary numbers (Import Instances.P) +- 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 |