From a1b828d31c73d3342345243e9fb4af69610616a0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 20 Oct 2015 18:15:04 +0200
Subject: Fix lemma-overloading

Update the evar_source of the solution evar in evar/evar problems to
propagate the information that it does not necessarily have to be solved
in Program mode.
---
 pretyping/evarsolve.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b384bdfe16..f06207c3b9 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1149,10 +1149,19 @@ let check_evar_instance evd evk1 body conv_algo =
   | Success evd -> evd
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
 
+let update_evar_source ev1 ev2 evd =
+  let loc, evs2 = evar_source ev2 evd in
+  match evs2 with
+  | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) ->
+     let evi = Evd.find evd ev1 in
+     Evd.add evd ev1 {evi with evar_source = loc, evs2}
+  | _ -> evd
+  
 let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
     let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
     let evd' = Evd.define evk2 body evd in
+    let evd' = update_evar_source (fst (destEvar body)) evk2 evd' in
       check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
     f env evd pbty ev2 c
@@ -1164,8 +1173,8 @@ let preferred_orientation evd evk1 evk2 =
   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
+  | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) , _ -> true
+  | _, (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> false
   | _ -> true
 
 let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
-- 
cgit v1.2.3