From 6c4fcb156dea5a71fd227606b87333ae00aacb69 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 29 Feb 2016 11:35:34 +0100
Subject: Moving the "generalize dependent" tactic to TACTIC EXTEND.

---
 intf/tacexpr.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index d936748f2d..52c07e089a 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -151,7 +151,6 @@ type 'a gen_atomic_tactic_expr =
       bool * 'tacexpr option *
       'dtrm intro_pattern_expr located option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
-  | TacGeneralizeDep of 'trm
   | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
       intro_pattern_naming_expr located option
 
-- 
cgit v1.2.3