Not "Setting ?n=?p order to ?p:=?n to see if it solves some

incompatibilities wrt 8.4.", as it creates other problems (in Ergo and
Compcert).

This reverts commit bf388dfec041ab0fa74ae5d484600f6fcf515e4f.

1 files changed, 8 insertions, 1 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f5d8baed91..078117fbd0 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1104,7 +1104,14 @@ 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 = false
+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 solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let aliases = make_alias_map env in