summaryrefslogtreecommitdiff
path: root/description
diff options
context:
space:
mode:
Diffstat (limited to 'description')
-rw-r--r--description15
1 files changed, 15 insertions, 0 deletions
diff --git a/description b/description
new file mode 100644
index 0000000..7b7195d
--- /dev/null
+++ b/description
@@ -0,0 +1,15 @@
+Name: AACTactics
+Title: AAC tactics
+Description: This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators:
+Keywords: reflexive tactic, rewriting, rewriting modulo associativity and commutativity, rewriting modulo AC, reflexive decision procedure
+Category: Miscellaneous/Coq Extensions
+Author: Thomas Braibant
+Email: thomas.braibant@gmail.com
+Homepage: http://sardes.inrialpes.fr/~braibant/
+Institution: INRIA/UJF/Ens Lyon
+Author: Damien Pous
+Email: damien.pous@inria.fr
+Homepage: http://sardes.inrialpes.fr/~pous/
+Institution: CNRS
+Require:
+License: LGPL