From efa921c807e48cfc19943d2bfd7f4eb11f8f9e09 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 24 Jun 2014 02:01:52 +0200
Subject: Extra check for indirect dependency when abstracting a term which is
 not a variable, in the future objective to factorize code between "generalize
 dependent" and "set", "destruct", etc.

---
 tactics/tactics.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 450b48d455..30568edab4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -660,11 +660,6 @@ let rec intros_move = function
       Tacticals.New.tclTHEN (intro_gen dloc (IntroMustBe hyp) destopt false false)
 	(intros_move rest)
 
-let dependent_in_decl a (_,c,t) =
-  match c with
-    | None -> dependent a t
-    | Some body -> dependent a body || dependent a t
-
 (* Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
 
-- 
cgit v1.2.3