A tentative fix for #4413

pretyping/evarsolve.ml

@@ -1267,13 +1267,7 @@ let solve_evar_evar_l2r force 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 _ | Evar_kinds.ImplicitArg (_, _, false)) , _ -> true
-  | _, (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> false
-  | _ -> true
+  List.mem evk1 (Evd.future_goals evd) || not (List.mem evk2 (Evd.future_goals evd))
 
 let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let aliases = make_alias_map env evd in

test-suite/bugs/closed/4095.v

@@ -71,7 +71,7 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
     refine (P _ _)
   end.
   Undo.
-  Fail lazymatch goal with
+  lazymatch goal with
   | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
     let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in
     set(p:=P)
@@ -84,4 +84,4 @@ O1 : T -> PointedOPred
 tr : T -> T
 O2 : PointedOPred
 x0 : T
-H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
+H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)

test-suite/bugs/closed/4413.v

@@ -0,0 +1,8 @@
+(* Regression wrt v8.4 related to the change of order of resolution of evar-evar unification problems. *)
+
+Goal exists x, x=1 -> True.
+eexists. intro H.
+pose proof (f_equal (fun k => k) H).
+Undo.
+pose (@f_equal _ _ S _ _ H).
+Abort.