Replace uses of Termops.dependent by more specific functions.

This is more efficient in general, because Termops.dependent doesn't take
advantage of the knowledge of its pattern argument.

8 files changed, 36 insertions, 22 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index b7531f6fc..e9d17e3c5 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -851,6 +851,13 @@ let occur_meta_or_existential sigma c =
     | _ -> EConstr.iter sigma occrec c
   in try occrec c; false with Occur -> true
 
+let occur_metavariable sigma m c =
+  let rec occrec c = match EConstr.kind sigma c with
+  | Meta m' -> if Int.equal m m' then raise Occur
+  | _ -> EConstr.iter sigma occrec c
+  in
+  try occrec c; false with Occur -> true
+
 let occur_evar sigma n c =
   let rec occur_rec c = match EConstr.kind sigma c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
diff --git a/engine/termops.mli b/engine/termops.mli
index 3b0c4bba6..54b47f9e4 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -94,6 +94,7 @@ exception Occur
 val occur_meta : Evd.evar_map -> constr -> bool
 val occur_existential : Evd.evar_map -> constr -> bool
 val occur_meta_or_existential : Evd.evar_map -> constr -> bool
+val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool
 val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
 val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
 val occur_var_in_decl :
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index b869c04a2..27abc3cc1 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -56,12 +56,12 @@ let unif evd t1 t2=
 	  | Meta i,_ ->
 	      let t=subst_meta !sigma nt2 in
 		if Int.Set.is_empty (free_rels evd t) &&
-		  not (dependent evd (EConstr.mkMeta i) t) then
+                  not (occur_metavariable evd i t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | _,Meta i ->
 	      let t=subst_meta !sigma nt1 in
 		if Int.Set.is_empty (free_rels evd t) &&
-		  not (dependent evd (EConstr.mkMeta i) t) then
+                  not (occur_metavariable evd i t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige
  	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 73be9d6b7..de2e735c7 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
@@ -1936,8 +1938,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. *) ->
@@ -1948,13 +1950,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 96d80741a..484ecea7e 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -527,7 +527,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 ->
@@ -1072,8 +1072,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 *)
@@ -1081,9 +1087,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 f2f922fd5..7d5688f7b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -699,7 +699,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
@@ -719,7 +719,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
@@ -1506,7 +1506,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
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 98f627f21..75b76695c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1800,9 +1800,9 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
     (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
     if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else
       match EConstr.kind sigma x, EConstr.kind sigma y with
-      | Var x', _ when not (dependent sigma x y) && not (is_evaluable env (EvalVarRef x')) ->
+      | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) ->
           subst_one flags.rewrite_dependent_proof x' (hyp,y,true)
-      | _, Var y' when not (dependent sigma y x) && not (is_evaluable env (EvalVarRef y')) ->
+      | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) ->
           subst_one flags.rewrite_dependent_proof y' (hyp,x,false)
       | _ ->
           Proofview.tclUNIT ()
diff --git a/tactics/inv.ml b/tactics/inv.ml
index d76c9a697..590098bdc 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -470,7 +470,7 @@ let raw_inversion inv_kind id status names =
       make_inv_predicate env evdref indf realargs id status concl in
     let sigma = !evdref in
     let (cut_concl,case_tac) =
-      if status != NoDep && (dependent sigma c concl) then
+      if status != NoDep && (local_occur_var sigma id concl) then
         Reductionops.beta_applist sigma (elim_predicate, realargs@[c]),
         case_then_using
       else