The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi Jason,

I'll look at your file soon, but let me first address your PS:

On Wed, Mar 13, 2013 at 6:32 AM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
>
> P.S. What's the difference between how ssreflect tactics use canonical
> structures, and how standard tactics use canonical structures?
>

For what I understand, it has to do with the fact that Coq has two
unification algorithms. Ssreflect's tactics use systematically one of
them, while Coq's apply, for instance, may end up using the two,
making unification seriously unpredictable. And canonical structures
are baked into the unification algorithm so predictability is crucial.

Cheers,
Beta