From 3b85b2bb48261ed262106e5591fa459bd3d94d73 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 3 Dec 2014 13:07:35 +0100 Subject: 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. --- pretyping/evarsolve.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping') 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 -- cgit v1.2.3