Yet another source of dependency on alphabetic order in unification

[herbelin]

Description of the problem

In the following examples, the return clause is not resolved the same for the two calls to refine:

Lemma foo (n1 n2: nat) (e: n1 = n2) : e = e.
refine (match e as a in _ = b return _ with refl_equal => _ end).
(* gives "eq_refl = eq_refl" *)
Undo 1.
refine (match e as z in _ = y return _ with refl_equal => _ end).
(* gives "e = e" *)

This is observable since version 8.4. Fix coming.