diff options
| author | Pierre Courtieu | 2002-05-29 18:45:45 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2002-05-29 18:45:45 +0000 |
| commit | 650a65abe40ce22ba896037bee3bab41fb69a118 (patch) | |
| tree | c95eb9fe7ddb8f1dd91eb1346e7479fdbc05b326 | |
| parent | 19d8306f9dab9d2d7a5cc8067a9bdaef8e1e2067 (diff) | |
Added some new tactic names
| -rw-r--r-- | coq/coq-syntax.el | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 898cc17d..870b578b 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -72,6 +72,8 @@ (defvar coq-keywords-not-undoable-commands '( "(*" ;;Pierre comments must not be undone +"Add\\s-+LoadPath" +"Add\\s-+Rec\\s-+LoadPath" "Add\\s-+ML\\s-+Path" "AddPath" "Begin\\s-+Silent" @@ -94,6 +96,7 @@ "Hint" "Infix" "Initialize" +"Implicits";; undoable?? "Implicit\\s-+Arguments\\s-+On" "Implicit\\s-+Arguments\\s-+Off" "Load" @@ -120,6 +123,8 @@ "Reset" "Search" "SearchIsos" +"SearchPattern" +"SearchRewrite" ;; da: testing moving this ;; "Section" "Show\\s-+Programs" @@ -143,12 +148,14 @@ '( "Absurd" "Apply" +"Assert" "Assumption" "Auto" "AutoRewrite" "Case" "Change" "Clear" +"ClearBody" "Cofix" "Compute" "Constructor" @@ -167,6 +174,8 @@ "Elim" "Exact" "Exists" +"Field" +"Fourier" "Fix" "Generalize" "Hnf" @@ -178,16 +187,21 @@ "Inversion" "LApply" "Left" +"LetTac" "Linear" "Load" +"NewDestruct" +"NewInduction" "Omega" "Pattern" +"Pose" "Program_all" "Program" "Prolog" "Realizer" "Red" "Reflexivity" +"Rename" "Replace" "Rewrite" "Right" @@ -229,6 +243,7 @@ "Fix" "if" "in" + "into" "let" "of" "then" |