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/evarconv.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/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 7 |
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 = |