From 0cf1f6447870998d0b58667d4dbe1c65faa3b723 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 Dec 2014 19:14:51 +0100
Subject: Tentatively starting to use heuristics for evar-evar resolution:
 first step, prefer QuestionMark's to other evars, to comply with the
 filtering made on VarInstance, GoalEvar and QuestionMark for type class
 resolution. Maybe evars to be resolved by type class instances should
 eventually be marked with a specific tag.

At least, this solves the current problem with compiling cancel2.v in
LemmaOverloading.
---
 pretyping/evarsolve.ml | 26 +++++++++++++++++++++-----
 1 file changed, 21 insertions(+), 5 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3f2eacf879..48fab0dfdc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1104,13 +1104,29 @@ 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 solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let aliases = make_alias_map env in
-  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
+  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) ->
+    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) ->
+    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) =
   let (evd,ev1,ev2),pbty =
-- 
cgit v1.2.3