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