summaryrefslogtreecommitdiff
path: root/ide/coq_tactics.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /ide/coq_tactics.ml
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'ide/coq_tactics.ml')
-rw-r--r--ide/coq_tactics.ml131
1 files changed, 131 insertions, 0 deletions
diff --git a/ide/coq_tactics.ml b/ide/coq_tactics.ml
new file mode 100644
index 00000000..4dd20b47
--- /dev/null
+++ b/ide/coq_tactics.ml
@@ -0,0 +1,131 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: coq_tactics.ml,v 1.2.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+
+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";
+]