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.

  One more question.
  Can you please explain briefly, what these
algorithms are, and what's the difference between
"apply rsimplify_morphisms." and
"refine (rsimplify_morphisms _)."?