This refines even further c24bcae (PR coq#924) and 6304c84:
- c24bcae fixed the order in the heuristic
- 6304c84 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.