diff options
author | 2003-03-05 14:37:25 +0000 | |
---|---|---|
committer | 2003-03-05 14:37:25 +0000 | |
commit | c019ddbb37a35b911b49437e20359d15563cdd7b (patch) | |
tree | 23813576acf53f3ece27b14ab99791d9620ce251 /ide/coq_tactics.ml | |
parent | bd6e68f4ef7bac1e9729b875f944048b394e71af (diff) |
IDE: menu templates
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3742 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq_tactics.ml')
-rw-r--r-- | ide/coq_tactics.ml | 124 |
1 files changed, 124 insertions, 0 deletions
diff --git a/ide/coq_tactics.ml b/ide/coq_tactics.ml new file mode 100644 index 000000000..7cac14da4 --- /dev/null +++ b/ide/coq_tactics.ml @@ -0,0 +1,124 @@ +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"; +] + + + |