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

this package provides the static native-code library, needed to build custom toplevels, and the compiled interfaces.