Bug#605487: ITP: aac-tactics -- Coq tactics for reasoning modulo AC

[Stéphane Glondu <steph@glondu.net>]

Package: wnpp
Severity: wishlist
Owner: "Stéphane Glondu" <steph@glondu.net>

* Package name    : aac-tactics
  Version         : 0.1
  Upstream Author : Thomas Braibant, Damien Pous
* URL             : http://sardes.inrialpes.fr/~braibant/aac_tactics/
* License         : LGPL-3+
  Programming Lang: OCaml, Coq
  Description     : Coq tactics for reasoning modulo AC

 This Coq plugin provides tactics for rewriting universally quantified
 equations, modulo associative (and possibly commutative) operators.