Blaisorblade is right, these papers are about a third algorithm, available via the UniCoq plugin, which is a cleaner, documented, and almost backward compatible, version of
evarconv.ml. It is still slower, last time we checked (not algorithmically, it was due to simpler data structures IIRC) so we could not replace
evarconv.ml with it.
I think we need Matthieu to know exactly the differences. From far away, also in time,
Metas and not
Evars (you still find that node in the internal syntax of terms).
Metas are not assigned a type and don't track which bound variables are in scope. This is a funny beast for a type theoretic system. Indeed you can't possibly implement HO unification in a sound way with them.
evarconv.ml is based on
Evars, which do have a type and an explicit substitution to make reduction and instantiation commute. So
evarconv.ml definitely makes more sense than
unification.ml, but, coding style on the side, it has still a few downsides, in particular it may suspend/resume hard unification (sub) problems in unpredictable ways.
All SSReflect tactics use
evarconv.ml since I can remember. Most of the vanilla tactics were progressively ported to
evarconv.ml as well, with the notable exception of
apply which is still "in progress" (there is a series of PRs called "unifall", not all merged).
I don't think you can compare unification in isolation. It is used inside elaboration (say, type inference). IIRC Agda has an algorithm based on accumulating (unification) constraints during typing, and then solving them in a "good" order. Lean used to have a similar approach (it is described in a paper) but that part of the system got rewritten. In Coq,
pretyping.ml does solve unification problems via
evarconv.ml eagerly, with some exceptions in which the problem is postponed (since it is too loosely constrained to hint to a single solution) and eventually resumed when made more constrained by some related
Evar assignment or when the client forcibly asks for a solution, not necessarily the only one.