IDE: menu templates

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

1 files changed, 182 insertions, 0 deletions

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
new file mode 100644
index 000000000..773fe54f6
--- /dev/null
+++ b/ide/coq_commands.ml
@@ -0,0 +1,182 @@
+let commands = [
+  "Abort";
+  "Add Abstract Ring";
+  "Add Abstract Semi Ring";
+  "Add Field";
+  "Add LoadPath";
+  "Add ML Path";
+  "Add Morphism";
+  "Add Printing If ident";
+  "Add Printing Let ident";
+  "Add Rec LoadPath";
+  "Add Rec ML Path";
+  "Add Ring";
+  "Add Semi Ring";
+  "Add Semi Ring";
+  "Add Setoid";
+  "Axiom";
+  "Back";
+  "Begin Silent";
+  "Canonical Structure";
+  "Cd";
+  "Chapter";
+  "Check";
+  "Coercion";
+  "Coercion Local";
+  "CoFixpoint";
+  "CoInductive";
+  "Correctness";
+  "Declare ML Module";
+  "Defined";
+  "Definition";
+  "Derive Dependent Inversion";
+  "Derive Dependent Inversion_clear";
+  "Derive Inversion";
+  "Derive Inversion_clear";
+  "Drop";
+  "End";
+  "End Silent";
+  "Eval";
+  "Explicitation of implicit arguments";
+  "Extract Constant";
+  "Extract Inductive";
+  "Extraction";
+  "Extraction Inline";
+  "Extraction Language";
+  "Extraction Module";
+  "Extraction NoInline";
+  "Fact";
+  "Fixpoint";
+  "Focus";
+  "Global Variable";
+  "Goal";
+  "Grammar";
+  "Hint;
+    * Hint Constructors";
+  "Hint Unfold";
+  "Hint";
+  "Hint Rewrite";
+  "Hints Extern";
+  "Hints Immediate";
+  "Hints Resolve";
+  "Hints Immediate";
+  "Hints Resolve";
+  "Hints Unfold";
+  "Hypothesis";
+  "Identity Coercion";
+  "Implicit Arguments Off";
+  "Implicit Arguments On";
+  "Implicits";
+  "Inductive";
+  "Infix";
+  "Inspect";
+  "Lemma";
+  "Load";
+  "Load Verbose";
+  "Local";
+  "Locate";
+  "Locate File";
+  "Locate Library";
+  "Module";
+  "Module Type";
+  "Mutual Inductive";
+  "Notation";
+  "Opaque";
+  "Parameter";
+  "Print";
+  "Print All";
+  "Print Classes";
+  "Print Coercion Paths";
+  "Print Coercions";
+  "Print Extraction Inline";
+  "Print Graph";
+  "Print Hint";
+  "Print HintDb";
+  "Print LoadPath";
+  "Print ML Modules";
+  "Print ML Path";
+  "Print Module";
+  "Print Module Type";
+  "Print Modules";
+  "Print Proof";
+  "Print Section";
+  "Print Table Printing If";
+  "Print Table Printing Let";
+  "Proof";
+  "Pwd";
+  "Qed";
+  "Quit";
+  "Read Module";
+  "Record";
+  "Recursive Extraction";
+  "Recursive Extraction Module";
+  "Remark";
+  "Remove LoadPath";
+  "Remove Printing If ident";
+  "Remove Printing Let ident";
+  "Require";
+  "Require Export";
+  "Reset";
+  "Reset Extraction Inline";
+  "Reset Initial";
+  "Restart";
+  "Restore State";
+  "Resume";
+  "Save";
+  "Scheme";
+  "Search";
+  "Search ... inside ...";
+  "Search ... outside ...";
+  "SearchAbout";
+  "SearchPattern";
+  "SearchPattern ... inside ...";
+  "SearchPattern ... outside ...";
+  "SearchRewrite";
+  "SearchRewrite ... inside ...";
+  "SearchRewrite ... outside ...";
+  "Section";
+  "Set Extraction AutoInline";
+  "Set Extraction Optimize";
+  "Set Hyps_limit";
+  "Set Implicit Arguments";
+  "Set Printing Coercion";
+  "Set Printing Coercions";
+  "Set Printing Synth";
+  "Set Printing Wildcard";
+  "Set Undo";
+  "Show";
+  "Show Conjectures";
+  "Show Implicits";
+  "Show Intro";
+  "Show Intros";
+  "Show Programs";
+  "Show Proof";
+  "Show Script";
+  "Show Tree";
+  "Structure";
+  "Suspend";
+  "Syntactic Definition";
+  "Syntax";
+  "Tactic Definition";
+  "Test Printing If ident";
+  "Test Printing Let ident";
+  "Test Printing Synth";
+  "Test Printing Wildcard";
+  "Theorem";
+  "Time";
+  "Transparent";
+  "Undo";
+  "Unfocus";
+  "Unset Extraction AutoInline";
+  "Unset Extraction Optimize";
+  "Unset Hyps_limit";
+  "Unset Implicit Arguments";
+  "Unset Printing Coercion";
+  "Unset Printing Coercions";
+  "Unset Printing Synth";
+  "Unset Printing Wildcard";
+  "Unset Undo";
+  "Variable";
+  "Variables";
+  "Write State";
+]