Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 406 insertions, 0 deletions

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
new file mode 100644
index 00000000..1169d438
--- /dev/null
+++ b/ide/coq_commands.ml
@@ -0,0 +1,406 @@
+(************************************************************************)
+(*  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_commands.ml,v 1.15.2.1 2004/07/16 19:30:20 herbelin Exp $ *)
+
+let commands = [
+  [(* "Abort"; *)
+   "Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T.";
+   "Add Abstract Semi Ring A Aplus Amult Aone Azero Aeq T.";
+   "Add Field";
+   "Add LoadPath";
+   "Add ML Path";
+   "Add Morphism";
+   "Add Printing If";
+   "Add Printing Let";
+   "Add Rec LoadPath";
+   "Add Rec ML Path";
+   "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. ";
+   "Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ].";
+   "Add Setoid";
+   "Axiom";];
+  [(* "Back"; *) ];
+  ["Canonical Structure";
+   "Chapter";
+   "Coercion";
+   "Coercion Local";
+   "CoFixpoint";
+   "CoInductive";
+  ];
+  ["Declare ML Module";
+   "Defined.";
+   "Definition";
+   "Derive Dependent Inversion";
+   "Derive Dependent Inversion__clear";
+   "Derive Inversion";
+   "Derive Inversion__clear";
+  ];
+  ["End";
+   "End Silent.";
+   "Eval"; 
+   "Extract Constant";
+   "Extract Inductive";
+   "Extraction Inline";
+   "Extraction Language";
+   "Extraction NoInline";];
+  ["Fact";
+   "Fixpoint";
+   "Focus";];
+  ["Global Variable";
+   "Goal";
+   "Grammar";];
+  ["Hint";
+   "Hint Constructors";
+   "Hint Extern";
+   "Hint Immediate";
+   "Hint Resolve";
+   "Hint Rewrite";
+   "Hint Unfold";
+   "Hypothesis";];
+  ["Identity Coercion";
+   "Implicits";
+   "Inductive";
+   "Infix";
+   ];
+  ["Lemma";
+   "Load";
+   "Load Verbose";
+   "Local";
+   "Ltac";
+  ];
+  ["Module";
+   "Module Type";
+   "Mutual Inductive";];
+  ["Notation";];
+  ["Opaque";];
+  ["Parameter";
+   "Proof."];
+  ["Qed.";
+   ];
+  ["Read Module";
+   "Record";
+   "Remark";
+   "Remove LoadPath";
+   "Remove Printing If";
+   "Remove Printing Let";
+   "Require";
+   "Require Export";
+   "Require Import";
+   "Reset Extraction Inline";
+   "Restore State"; 
+   ];
+  [  "Save.";
+     "Scheme";
+     "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 Silent.";
+     "Set Undo";
+     (*"Show";
+     "Show Conjectures";
+     "Show Implicits";
+     "Show Intro";
+     "Show Intros";
+     "Show Programs";
+     "Show Proof";
+     "Show Script";
+     "Show Tree";*)
+     "Structure";
+     (* "Suspend"; *)
+     "Syntactic Definition";
+     "Syntax";];
+  [
+   "Test Printing If";
+   "Test Printing Let";
+   "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 Silent.";
+   "Unset Undo";];
+  ["Variable";
+   "Variables";];
+  ["Write State";];
+]
+
+let state_preserving = [
+  "Check";
+  "Eval";
+  "Eval compute in";
+  "Extraction";
+  "Extraction Library";
+  "Extraction Module";
+  "Inspect";
+  "Locate";
+  "Print";
+  "Print All.";
+  "Print Classes";
+  "Print Coercion Paths";
+  "Print Coercions";
+  "Print Extraction Inline";
+  "Print Grammar";
+  "Print Graph";
+  "Print Hint";
+  "Print Hint *";
+  "Print HintDb";
+  "Print Implicit";
+  "Print LoadPath";
+  "Print ML Modules";
+  "Print ML Path";
+  "Print Module";
+  "Print Module Type";
+  "Print Modules";
+  "Print Proof";
+  "Print Scope";
+  "Print Scopes.";
+  "Print Section";
+  
+  "Print Table Printing If.";
+  "Print Table Printing Let.";
+  "Print Tables.";
+  "Print Term";
+
+  "Print Visibility";
+
+  "Pwd.";
+
+  "Recursive Extraction";
+  "Recursive Extraction Library";
+
+  "Search";
+  "SearchAbout";
+  "SearchPattern";
+  "SearchRewrite";
+
+  "Show";
+  "Show Conjectures";
+  "Show Implicits";
+  "Show Intro";
+  "Show Intros";
+  "Show Proof";
+  "Show Script";
+  "Show Tree";
+
+  "Test Printing If";
+  "Test Printing Let";
+  "Test Printing Synth";
+  "Test Printing Wildcard";
+]
+
+
+let tactics = 
+  [
+    [
+      "abstract";
+      "absurd";
+      "apply";
+      "apply __ with";
+      "assert";
+      "assert (__:__)";
+      "assert (__:=__)";
+      "assumption";
+      "auto";
+      "auto with";
+      "autorewrite";
+    ];
+
+   [
+     "case";
+     "case __ with";
+     "casetype";
+     "cbv";
+     "cbv in";
+     "change";
+     "change __ in";
+     "clear";
+     "clearbody";
+     "cofix";
+     "compare";
+     "compute";
+     "compute in";
+     "congruence";
+     "constructor";
+     "constructor __ with";
+     "contradiction";
+     "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 <-";
+     "destruct";
+     "discriminate";
+     "do";
+     "double induction";
+   ];
+
+   [
+     "eapply";
+     "eauto";
+     "eauto with";
+     "eexact";
+     "elim";
+     "elim __ using";
+     "elim __ with";
+     "elimtype";
+     "exact";
+     "exists";
+   ];
+
+   [
+     "fail";
+     "field";
+     "first";
+     "firstorder";
+     "firstorder using";
+     "firstorder with";
+     "fix";
+     "fix __ with";
+     "fold";
+     "fold __ in";
+     "fourier";
+     "functional induction";
+   ];
+
+   [
+     "generalize";
+     "generalize dependent";
+   ];
+   
+   [
+     "hnf";
+   ];
+
+   [
+     "idtac";
+     "induction";
+     "info";
+     "injection";
+     "instantiate (__:=__)";
+     "intro";
+     "intro after";
+     "intro __ after";
+     "intros";
+     "intros until";
+     "intuition";
+     "inversion";
+     "inversion __ in";
+     "inversion __ using";
+     "inversion __ using __ in";
+     "inversion__clear";
+     "inversion__clear __ in";
+   ];
+
+   [
+     "jp <n>";
+     "jp";
+   ];
+
+   [
+     "lapply";
+     "lazy";
+     "lazy in";
+     "left";
+   ];
+
+   [
+     "move __ after";
+   ];
+
+   [
+     "omega";
+   ];
+
+   [
+     "pattern";
+     "pose";
+     "pose __:=__)";
+     "progress";
+   ];
+
+   [
+     "quote";
+   ];
+
+   [
+     "red";
+     "red in";
+     "refine";
+     "reflexivity";
+     "rename __ into";
+     "repeat";
+     "replace __ with";
+     "rewrite";
+     "rewrite __ in";
+     "rewrite <-";
+     "rewrite <- __ in";
+     "right";
+     "ring";
+   ];
+
+   [
+     "set";
+     "set (__:=__)";
+     "setoid__replace";
+     "setoid__rewrite";
+     "simpl";
+     "simpl __ in";
+     "simple destruct";
+     "simple induction";
+     "simple inversion";
+     "simplify__eq";
+     "solve";
+     "split";
+(*     "split__Rabs";
+     "split__Rmult";
+*)
+     "subst";
+     "symmetry";
+     "symmetry in";
+   ];
+
+   [
+     "tauto";
+     "transitivity";
+     "trivial";
+     "try";
+   ];
+   
+   [
+     "unfold";
+     "unfold __ in";
+   ];
+]
+
+