Merge PR #7216: Replace uses of Termops.dependent by more specific functions.

3 files changed, 23 insertions, 17 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ee7c39982..38196489a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -574,7 +574,7 @@ let dependent_decl sigma a =
 
 let rec dep_in_tomatch sigma n = function
   | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch sigma n l
-  | Abstract (_,d) :: l -> dependent_decl sigma (mkRel n) d || dep_in_tomatch sigma (n+1) l
+  | Abstract (_,d) :: l -> RelDecl.exists (fun c -> not (noccurn sigma n c)) d || dep_in_tomatch sigma (n+1) l
   | [] -> false
 
 let dependencies_in_rhs sigma nargs current tms eqns =
@@ -1704,9 +1704,11 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
 	List.map_i
 	  (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1
 	  (rel_context extenv) in
-      let rel_filter =
-	List.map (fun a -> not (isRel !evdref a) || dependent !evdref a u
-                           || Int.Set.mem (destRel !evdref a) depvl) inst in
+      let map a = match EConstr.kind !evdref a with
+      | Rel n -> not (noccurn !evdref n u) || Int.Set.mem n depvl
+      | _ -> true
+      in
+      let rel_filter = List.map map inst in
       let named_filter =
 	List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u)
 	  (named_context extenv) in
@@ -1937,8 +1939,8 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
 	match EConstr.kind sigma tm with
-	  | Rel n when dependent sigma tm c
-		&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
+          | Rel n when Int.equal signlen 1 && not (noccurn sigma n c)
+            (* The term to match is not of a dependent type itself *) ->
 	      ((n, len) :: subst, len - signlen)
 	  | Rel n when signlen > 1 (* The term is of a dependent type,
 				      maybe some variable in its type appears in the tycon. *) ->
@@ -1949,13 +1951,13 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 		      List.fold_left
 			(fun (subst, len) arg ->
 			  match EConstr.kind sigma arg with
-			  | Rel n when dependent sigma arg c ->
+                          | Rel n when not (noccurn sigma n c) ->
 			      ((n, len) :: subst, pred len)
 			  | _ -> (subst, pred len))
 			(subst, len) realargs
 		    in
 		    let subst =
-		      if dependent sigma tm c && List.for_all (isRel sigma) realargs
+                      if not (noccurn sigma n c) && List.for_all (isRel sigma) realargs
 		      then (n, len) :: subst else subst
 		    in (subst, pred len))
 	  | _ -> (subst, len - signlen))
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b7eaff078..aefae1ecc 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -525,7 +525,7 @@ let is_unification_pattern_meta env evd nb m l t =
   match Option.List.map map l with
   | Some l ->
     begin match find_unification_pattern_args env evd l t with
-    | Some _ as x when not (dependent evd (mkMeta m) t) -> x
+    | Some _ as x when not (occur_metavariable evd m t) -> x
     | _ -> None
     end
   | None ->
@@ -1068,8 +1068,14 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
 
 let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
   let rhs = expand_vars_in_term env evd rhs in
-  let filter =
-    restrict_upon_filter evd evk
+  let filter a = match EConstr.kind evd a with
+  | Rel n -> not (noccurn evd  n rhs)
+  | Var id ->
+    local_occur_var evd id rhs
+      || List.exists (fun (id', _) -> Id.equal id id') sols
+  | _ -> true
+  in
+  let filter = restrict_upon_filter evd evk filter argsv in
       (* Keep only variables that occur in rhs *)
       (* This is not safe: is the variable is a local def, its body *)
       (* may contain references to variables that are removed, leading to *)
@@ -1077,9 +1083,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
       (* that says that the body is hidden. Note that expand_vars_in_term *)
       (* expands only rels and vars aliases, not rels or vars bound to an *)
       (* arbitrary complex term *)
-      (fun a -> not (isRel evd a || isVar evd a)
-                || dependent evd a rhs || List.exists (fun (id,_) -> isVarId evd id a) sols)
-      argsv in
   let filter = closure_of_filter evd evk filter in
   let candidates = extract_candidates sols in
   match candidates with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b9678fa10..b49291adb 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -698,7 +698,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	    if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst
 	    else sigma,(k2,cM,stM)::metasubst,evarsubst
 	| Meta k, _
-            when not (dependent sigma cM cN) (* helps early trying alternatives *) ->
+            when not (occur_metavariable sigma k cN) (* helps early trying alternatives *) ->
             let sigma = 
 	      if opt.with_types && flags.check_applied_meta_types then
 		(try
@@ -718,7 +718,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
               evarsubst)
 	    else error_cannot_unify_local curenv sigma (m,n,cN)
 	| _, Meta k
-            when not (dependent sigma cN cM) (* helps early trying alternatives *) ->
+            when not (occur_metavariable sigma k cM) (* helps early trying alternatives *) ->
           let sigma = 
 	    if opt.with_types && flags.check_applied_meta_types then
               (try
@@ -1500,7 +1500,8 @@ let indirectly_dependent sigma c d decls =
        it is needed otherwise, as e.g. when abstracting over "2" in
        "forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious
        way to see that the second hypothesis depends indirectly over 2 *)
-    List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls
+    let open Context.Named.Declaration in
+    List.exists (fun d' -> exists (fun c -> Termops.local_occur_var sigma (NamedDecl.get_id d') c) d) decls
 
 let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
   let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in