The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I'm not sure I understand your point, since [apply] and [match] use the same unification algorithm.

I don't think that's right, actually. Ltac's [match] does not do any unification, and the pattern-matching algorithm that it implements does not seem like it shares any code with apply's unification engine.