diff options
| author | Pierre-Marie Pédrot | 2018-09-19 10:22:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-19 10:22:07 +0200 |
| commit | c32c8e2b18ea76087d9dbdb2b56a550aae61c917 (patch) | |
| tree | 605efaebda1c9f19fecc025ddc01f9e0bdb632a7 /pretyping/cases.ml | |
| parent | 44b8c4ec9acad33002b080ed0aefb214124db440 (diff) | |
| parent | c9c18edee8664e0e52ece7ef0ff83955f4eadcbd (diff) | |
Merge PR #7257: Fixing yet a source of dependency on alphabetic order in unification.
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 2 |
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 |