From 96906c2a1ba9426271a4048bfa8b3991db51c192 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 19 Dec 2014 10:39:27 +0100
Subject: Back to the preferred ?n1:=?n2 order of evar-evar unification which
 got accidentally mixed up in 9aa416c0c6.

---
 pretyping/evarsolve.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 48fab0dfdc..1a1cd92ed6 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1116,16 +1116,16 @@ let preferred_orientation evd evk1 evk2 =
 let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let aliases = make_alias_map env in
   if preferred_orientation evd evk1 evk2 then
-    try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2
-    with CannotProject (evd,ev1) ->
     try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) ->
+    try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2
+    with CannotProject (evd,ev1) ->
     add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
   else
-    try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
-    with CannotProject (evd,ev2) ->
     try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
+    try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
+    with CannotProject (evd,ev2) ->
     add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
 
 let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
-- 
cgit v1.2.3