diff options
| author |  Benjamin Barenblat <bbaren@google.com> | 2019-02-13 20:40:51 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@google.com> | 2019-02-13 20:40:51 -0500 |
| commit | 2ee22055c510a56c3d040fe023d0884b183bd68c (patch) | |
| tree | 595eeed2159e90da8284b9e2d545430a61a60d04 /README | |
| parent | 7ecbed522b4b4a9829eb9bd7b3f36db53788a77c (diff) | |
| parent | 8018e923c75eb5504310864f821972f794b7d554 (diff) | |
Updated version 8.8.0+1.gbp069dc3b from 'upstream/8.8.0+1.gbp069dc3b'
with Debian dir 4ca0cfbbc73543887b10ee2613b222f51702e276
Diffstat (limited to 'README')
| -rw-r--r-- | README | 55 |
1 files changed, 0 insertions, 55 deletions
@@ -1,55 +0,0 @@ - - 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 |