Remove ide/coq_tactics.ml*

Unused and refers to pre-v8 tactics. Basically untouched since
2003. Most likely obsolete.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13507 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 0 insertions, 140 deletions

diff --git a/ide/coq_tactics.ml b/ide/coq_tactics.ml
deleted file mode 100644
index 7a865d5e2..000000000
--- a/ide/coq_tactics.ml
+++ /dev/null
@@ -1,129 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-let tactics = [
-  "Abstract";
-  "Absurd";
-  "Apply";
-  "Apply ... with";
-  "Assert";
-  "Assumption";
-  "Auto";
-  "AutoRewrite";
-  "Binding list";
-  "Case";
-  "Case ... with";
-  "Cbv";
-  "Change";
-  "Change ... in";
-  "Clear";
-  "ClearBody";
-  "Compare";
-  "Compute";
-  "Constructor";
-  "Constructor ... with";
-  "Contradiction";
-  "Conversion tactics";
-  "Cut";
-  "CutRewrite";
-  "Decide Equality";
-  "Decompose";
-  "Decompose Record";
-  "Decompose Sum";
-  "Dependent Inversion";
-  "Dependent Inversion ... with";
-  "Dependent Inversion_clear";
-  "Dependent Inversion_clear ... with";
-  "Dependent Rewrite ->";
-  "Dependent Rewrite <-";
-  "Derive Inversion";
-  "Destruct";
-  "Discriminate";
-  "DiscrR";
-  "Do";
-  "Double Induction";
-  "EApply";
-  "EAuto";
-  "Elim ... using";
-  "Elim ... with";
-  "ElimType";
-  "Exact";
-  "Exists";
-  "Fail";
-  "Field";
-  "First";
-  "Fold";
-  "Fourier";
-  "Generalize";
-  "Generalize Dependent";
-  "Print Hint";
-  "Hnf";
-  "Idtac";
-  "Induction";
-  "Info";
-  "Injection";
-  "Intro";
-  "Intro ... after";
-  "Intro after";
-  "Intros";
-  "Intros pattern";
-  "Intros until";
-  "Intuition";
-  "Inversion";
-  "Inversion ... in";
-  "Inversion ... using";
-  "Inversion ... using ... in";
-  "Inversion_clear";
-  "Inversion_clear ... in";
-  "LApply";
-  "Lazy";
-  "Left";
-  "LetTac";
-  "Move";
-  "NewDestruct";
-  "NewInduction";
-  "Omega";
-  "Orelse";
-  "Pattern";
-  "Pose";
-  "Prolog";
-  "Quote";
-  "Red";
-  "Refine";
-  "Reflexivity";
-  "Rename";
-  "Repeat";
-  "Replace ... with";
-  "Rewrite";
-  "Rewrite ->";
-  "Rewrite -> ... in";
-  "Rewrite <-";
-  "Rewrite <- ... in";
-  "Rewrite ... in";
-  "Right";
-  "Ring";
-  "Setoid_replace";
-  "Setoid_rewrite";
-  "Simpl";
-  "Simple Inversion";
-  "Simplify_eq";
-  "Solve";
-  "Split";
-  "SplitAbsolu";
-  "SplitRmult";
-  "Subst";
-  "Symmetry";
-  "Tacticals";
-  "Tauto";
-  "Transitivity";
-  "Trivial";
-  "Try";
-  "tactic macros";
-  "Unfold";
-  "Unfold ... in";
-]
diff --git a/ide/coq_tactics.mli b/ide/coq_tactics.mli
deleted file mode 100644
index 498a1bbc6..000000000
--- a/ide/coq_tactics.mli
+++ /dev/null
@@ -1,10 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-val tactics : string list
-
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 1ead88c8e..87b66baba 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -19,6 +19,5 @@ Gtk_parsing
 Undo
 Coq
 Coq_commands
-Coq_tactics
 Command_windows
 Coqide