The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Aug 01, 2014 at 06:21:40PM +0200, Hugo Herbelin wrote:
> example being in rewriting "x * (y * z)" which started to match
> expressions of the form "t * power x 2". I have no idea how common
> this would occur in arbitrary developments.

This is expected, ssr does some magic for that specific case.
See http://hal.inria.fr/docs/00/66/98/05/PDF/rew.pdf section 3.2.

Actually the implementation in the plugin is very ugly, and I probably
still have a unfinished branch somewhere with a better coding of the
same idea.

Ciao,
-- 
Enrico Tassi