From 2b9f73c7e86ac718c0ce4c47d6a24ffc2d01499d Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 30 Jan 2008 04:21:51 +0000
Subject: Work on dependent induction tactic and friends, finish the test-suite
 example

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10487 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.mli | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index db46c621ff..eb62f602aa 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -327,11 +327,4 @@ val tclABSTRACT : identifier option -> tactic -> tactic
 
 val admit_as_an_axiom : tactic
 
-val make_abstract_generalize :     'a ->
-    Names.identifier ->
-    Term.constr ->
-    Sign.rel_context ->
-    Term.types ->
-    Term.types list ->
-    Term.constr list -> Term.constr list -> Term.constr -> Term.constr
 val abstract_generalize : identifier -> tactic
-- 
cgit v1.2.3