The Coq mailing list

[Dmitry Grebeniuk <gdsfh1 AT gmail.com>]

Hello.

> 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.

  So, canonical structures are useless without
ssreflect, or user should just avoid using some
tactics like "apply" while using canonical structures?