Removing need for ensure_evar_independent by passing a force flag to is_constrainable_in to do the job of ensuring that ?p does not belong to the ti while solving ?p[...]:=?n[t1..tn].

1 files changed, 21 insertions, 38 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index c894f5717e..b01f29a40a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1017,7 +1017,7 @@ exception CannotProject of evar_map * existential
   of subterms to eventually discard so as to be allowed to keep ti.
 *)
 
-let rec is_constrainable_in top k (ev,(fv_rels,fv_ids) as g) t =
+let rec is_constrainable_in top force k (ev,(fv_rels,fv_ids) as g) t =
   let f,args = decompose_app_vect t in
   match kind_of_term f with
   | Construct ((ind,_),u) ->
@@ -1025,44 +1025,31 @@ let rec is_constrainable_in top k (ev,(fv_rels,fv_ids) as g) t =
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (is_constrainable_in false k g) params
-  | Ind _ -> Array.for_all (is_constrainable_in false k g) args
-  | Prod (_,t1,t2) -> is_constrainable_in false k g t1 && is_constrainable_in false k g t2
-  | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
+      Array.for_all (is_constrainable_in false force k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in false force k g) args
+  | Prod (_,t1,t2) -> is_constrainable_in false force k g t1 && is_constrainable_in false force k g t2
+  | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
   | Sort _ -> true
   | _ -> (* We don't try to be more clever *) true
 
-let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
+let has_constrainable_free_vars evd aliases force k ev (fv_rels,fv_ids as fvs) t =
   let t = expansion_of_var aliases t in
   match kind_of_term t with
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
-  | _ -> is_constrainable_in true k (ev,fvs) t
-
-let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
-  let filter1 =
-    restrict_upon_filter evd evk1 (noccur_evar env evd evk2) argsv1
-  in
-  let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
-  let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
-  let filter2 =
-    restrict_upon_filter evd evk2 (noccur_evar env evd evk1) argsv2
-  in
-  let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
-  let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
-  evd,ev1,ev2
+  | _ -> is_constrainable_in true force k (ev,fvs) t
 
 exception EvarSolvedOnTheFly of evar_map * constr
 
 (* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on
    the common domain of definition *)
-let project_evar_on_evar g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
+let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
   (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
   let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
   let filter1 = restrict_upon_filter evd evk1
-    (has_constrainable_free_vars evd aliases k2 evk2 fvs2)
+    (has_constrainable_free_vars evd aliases force k2 evk2 fvs2)
     argsv1 in
   let candidates1 =
     try restrict_candidates g env evd filter1 ev1 ev2
@@ -1098,9 +1085,9 @@ let check_evar_instance evd evk1 body conv_algo =
   | Success evd -> evd
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
 
-let solve_evar_evar_l2r f g env evd aliases pbty ev1 (evk2,_ as ev2) =
+let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
-    let evd,body = project_evar_on_evar g env evd aliases 0 pbty ev1 ev2 in
+    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
       check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
@@ -1117,27 +1104,23 @@ let preferred_orientation evd evk1 evk2 =
   | _,Evar_kinds.QuestionMark _ -> false
   | _ -> true
 
-let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
+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 in
   if preferred_orientation evd evk1 evk2 then
-    try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
+    try solve_evar_evar_l2r force 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
+    try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
     add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
   else
-    try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2
+    try solve_evar_evar_l2r force 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
+    try solve_evar_evar_l2r force 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
 
-let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 =
-  let (evd,(evk1,args1 as ev1),(evk2,args2 as ev2)),pbty =
-    (* If an evar occurs in the instance of the other evar and the
-       use of an heuristic is forced, we restrict *)
-    if force then ensure_evar_independent g env evd ev1 ev2, None
-    else (evd,ev1,ev2),pbty in
+let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
+  let pbty = if force then None else pbty in
   let evi = Evd.find evd evk1 in
   let evd =
     try 
@@ -1166,7 +1149,7 @@ let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 =
           downcast evk2 t2 (downcast evk1 t1 evd)
     with Reduction.NotArity -> 
       evd in
-  solve_evar_evar_aux f g env evd pbty ev1 ev2
+  solve_evar_evar_aux force f g env evd pbty ev1 ev2
 
 type conv_fun =
   env ->  evar_map -> conv_pb -> constr -> constr -> unification_result
@@ -1325,7 +1308,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         let aliases = lift_aliases k aliases in
         (try
           let ev = (evk,Array.map (lift k) argsv) in
-          let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k None ev' ev in
+          let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in
           evdref := evd;
           body
         with
@@ -1342,7 +1325,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           let evd =
              (* Try to project (a restriction of) the left evar ... *)
             try
-              let evd,body = project_evar_on_evar conv_algo env' evd aliases 0 None ev'' ev' in
+              let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in
               let evd = Evd.define evk' body evd in
 		check_evar_instance evd evk' body conv_algo
             with