Fixing yet a source of dependency on alphabetic order in unification.

This refines even further c24bcae8 (PR #924) and 6304c843:
- c24bcae8 fixed the order in the heuristic
- 6304c843 improved the order by preferring projections

There remained a dependency in the alphabetic order in selecting
unification candidates. The current commit fixes it.

We radically change the representation of the substitution to invert
by using a map indexed on the rank in the signature rather than on the
name of the variable.

More could be done to use numbers further, e.g. for representing
aliases.

Note that this has consequences on the test-suite (in
output/Notations.v) as some problems now infer a dependent return
clause.

1 files changed, 1 insertions, 1 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7baa755ab5..81e8bd06f5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1726,7 +1726,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
 	List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u)
           (named_context !!extenv) in
       let filter = Filter.make (rel_filter @ named_filter) in
-      let candidates = u :: List.map mkRel vl in
+      let candidates = List.rev (u :: List.map mkRel vl) in
       let ev = evd_comb1 (Evarutil.new_evar !!extenv ~src ~filter ~candidates) evdref ty in
       lift k ev
   in