The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

> I guess users of Canonical Structures may have had a similar problem.
> Application of the [rewrite] lemma on the simplified goal would require
> infering "back" the [Twiddle_bar] record during unification. The ssreflect
> [rewrite] might be able to do that (simply declaring [Twiddle_bar] as
> canonical in Coq doesn't work of course).

   Indeed, the ssr [rewrite] can do this; it inherits this capability from 
the Coq type inference unification code, which it calls to pick redexes and 
apply rewrite rules ("classic" Coq tactics call a completely different 
unification routine). Much of what we've developped simply wouldn't work 
without this feature, including the "big operator" library we presented at 
TPHOL'08.

Cheers,
-- Georges