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, 6 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index ff242fe285..46266a1bd0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -75,6 +75,12 @@ Focusing
   e.g. `[x]: {` will focus on a goal (existential variable) named `x`.
   As usual, unfocus with `}` once the sub-goal is fully solved.
 
+Specification language
+
+- A fix to unification (which was sensitive to the ascii name of
+  variables) may occasionally change type inference in incompatible
+  ways, especially regarding the inference of the return clause of "match".
+
 Standard Library
 
 - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,