From bf388dfec041ab0fa74ae5d484600f6fcf515e4f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 8 Jan 2015 18:32:05 +0100
Subject: Setting ?n=?p order to ?p:=?n to see if it solves some
 incompatibilities wrt 8.4.

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

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 078117fbd0..f5d8baed91 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1104,14 +1104,7 @@ let solve_evar_evar_l2r f g env evd aliases pbty ev1 (evk2,_ as ev2) =
 
 let opp_problem = function None -> None | Some b -> Some (not b)
 
-let preferred_orientation evd evk1 evk2 =
-  let _,src1 = (Evd.find_undefined evd evk1).evar_source in
-  let _,src2 = (Evd.find_undefined evd evk2).evar_source in
-  (* This is a heuristic useful for program to work *)
-  match src1,src2 with
-  | Evar_kinds.QuestionMark _, _ -> true
-  | _,Evar_kinds.QuestionMark _ -> false
-  | _ -> true
+let preferred_orientation evd evk1 evk2 = false
 
 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
-- 
cgit v1.2.3