From 8018e923c75eb5504310864f821972f794b7d554 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Wed, 13 Feb 2019 20:40:51 -0500 Subject: New upstream version 8.8.0+1.gbp069dc3b --- README | 55 ------------------------------------------------------- 1 file changed, 55 deletions(-) delete mode 100644 README (limited to 'README') diff --git a/README b/README deleted file mode 100644 index 38fc514..0000000 --- a/README +++ /dev/null @@ -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 -- cgit v1.2.3