diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-03 13:07:35 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-03 19:24:13 +0100 |
| commit | 3b85b2bb48261ed262106e5591fa459bd3d94d73 (patch) | |
| tree | 5d0b721bce2483fc59ebb9639316a23fe2f21c07 /pretyping | |
| parent | e2fa65fccb9d55ea0b6bd5873155abf436785b1f (diff) | |
In solve_evar_evar, orient the heuristic over arities with different
types as it was before commit 710bae2a8c81a44.
There is still at least one problem with bug #3392 to solve.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 328bc3bdd..940eebbf7 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1146,9 +1146,9 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar solve_evar_evar_aux f g env evd pbty ev1 ev2 (* Avoid looping if postponing happened on previous evar/evar problem *) else if Evd.check_leq evd ui uj then - solve_evar_evar_aux f g env evd pbty ev1 ev2 - else if Evd.check_leq evd uj ui then solve_evar_evar_aux f g env evd (opp_problem pbty) ev2 ev1 + else if Evd.check_leq evd uj ui then + solve_evar_evar_aux f g env evd pbty ev1 ev2 else let evd, k = Evd.new_sort_variable univ_flexible_alg evd in let evd, ev3 = @@ -1157,8 +1157,8 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar ?candidates:evi.evar_candidates (it_mkProd_or_LetIn (mkSort k) ctx) in let evd = Evd.set_leq_sort env (Evd.set_leq_sort env evd k i) k j in - let evd = solve_evar_evar_aux f g env evd pbty ev1 (ev3,args1) in - f env evd (opp_problem pbty) ev2 (whd_evar evd (mkEvar (ev3,args1))) + let evd = solve_evar_evar_aux f g env evd (opp_problem pbty) (ev3,args1) ev1 in + f env evd (opp_problem pbty) ev2 (whd_evar evd (mkEvar (ev3,args1))) with Reduction.NotArity -> solve_evar_evar_aux f g env evd pbty ev1 ev2 |