From 99ffdbbdbf2b6d5be9d5346167e63e89d8e0ee74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Apr 2018 15:18:17 +0200
Subject: 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.
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/cases.ml')

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
-- 
cgit v1.2.3