From 7d6d9c5aea6232200b99e828b7e04b49808f8478 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 19 Oct 2015 18:13:32 +0200
Subject: Do occur-check w.r.t existential's types also when instantiating an
 evar.

---
 pretyping/evarsolve.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index bbc4f1db29..b384bdfe16 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1272,6 +1272,15 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs =
           restrict_evar evd evk None (UpdateWith candidates)
       | l -> evd
 
+let occur_evar_upto_types sigma n c =
+  let rec occur_rec c = match kind_of_term c with
+    | Evar (sp,_) when Evar.equal sp n -> raise Occur
+    | Evar e -> Option.iter occur_rec (existential_opt_value sigma e);
+		occur_rec (existential_type sigma e)
+    | _ -> iter_constr occur_rec c
+  in
+  try occur_rec c; false with Occur -> true
+
 (* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times
  * (i.e. we tackle a generalization of Miller-Pfenning patterns unification)
@@ -1459,7 +1468,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
 	  (recheck_applications conv_algo (evar_env evi) evdref t'; t')
 	else t'
   in (!evdref,body)
-
+     
 (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
  * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
  * [define] tries to find an instance lhs such that
@@ -1484,7 +1493,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
     if occur_meta body then raise MetaOccurInBodyInternal;
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
-    if occur_evar_upto evd' evk body then raise (OccurCheckIn (evd',body));
+    if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body));
     (* needed only if an inferred type *)
     let evd', body = refresh_universes pbty env evd' body in
 (* Cannot strictly type instantiations since the unification algorithm
-- 
cgit v1.2.3


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(-)

(limited to 'pretyping')

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