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, 4 insertions, 3 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 984fa92c0e..6c52dacaa9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1317,6 +1317,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
       let rec aux = function
       | [] -> user_err Pp.(str "Unsolvable existential variables.")
       | a::l ->
+          (* In case of variables, most recent ones come first *)
           try
             let conv_algo = evar_conv_x ts in
             let evd = check_evar_instance evd evk a conv_algo in
@@ -1327,9 +1328,9 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
           with
           | IllTypedInstance _ -> aux l
           | e when Pretype_errors.precatchable_exception e -> aux l in
-      (* List.rev is there to favor most dependent solutions *)
-      (* and favor progress when used with the refine tactics *)
-      let evd = aux (List.rev l) in
+      (* Expected invariant: most dependent solutions come first *)
+      (* so as to favor progress when used with the refine tactics *)
+      let evd = aux l in
       solve_unconstrained_evars_with_candidates ts evd
 
 let solve_unconstrained_impossible_cases env evd =