Added some unknown keyword (not changing state). Fixes bug 113 from emakarov.M

2 files changed, 26 insertions, 6 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 164ac4a5..78863d27 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -97,9 +97,9 @@
       ["Check..." coq-Check t]
       ["About..." coq-About t]
       ["Search..." coq-SearchConstant t]
-      ["Search Rewrite..." coq-SearchRewrite t]
-      ["Search About..." coq-SearchAbout t]
-      ["Search isos/pattern..." coq-SearchIsos t]
+      ["SearchRewrite..." coq-SearchRewrite t]
+      ["SearchAbout..." coq-SearchAbout t]
+      ["SearchPattern..." coq-SearchIsos t]
       ["Locate constant..." coq-LocateConstant t]
       ["Locate Library..." coq-LocateLibrary t]
       ["Pwd" coq-Pwd t]
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 84f28df3..cf72ecac 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -381,6 +381,8 @@ so for the following reasons:
    coq-user-commands-db
    '(
      ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu
+     ("About" nil "About #." nil "About")
+     ("Add" nil "Add #." nil "Add" nil t)
      ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring")
      ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring")
      ("Add Field" nil "Add Field #." t "Add\\s-+Field")
@@ -388,6 +390,8 @@ so for the following reasons:
      ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path")
      ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism")
      ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing")
+     ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If")
+     ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let")
      ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath")
      ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path")
      ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring")
@@ -396,8 +400,8 @@ so for the following reasons:
      ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope")
      ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope")
      ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure")
-     ("Cd" nil "Cd #." "Cd")
-     ("Check" nil "Check" "Check")
+     ("Cd" nil "Cd #." nil "Cd")
+     ("Check" nil "Check" nil "Check")
      ("Close Local Scope" "cllsc" "Close Local Scope #" t "Close\\s-+Local\\s-+Scope")
      ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope")
      ("Comments" nil "Comments #." nil "Comments")
@@ -407,7 +411,7 @@ so for the following reasons:
      ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant")
      ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract")
      ("Extraction" "extr" "Extraction @{id}." nil "Extraction")
-     ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}.")
+     ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil)
      ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline")
      ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline")
      ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language")
@@ -436,15 +440,22 @@ so for the following reasons:
      ("Print" "p" "Print #." nil "Print")
      ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint)
      ("Qed" nil "Qed." nil "Qed")
+     ("Pwd" nil "Pwd." nil "Pwd")
      ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction")
      ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library")
      ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module")
      ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath")
      ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath")
+     ("Remove Printing If" nil "Remove Printing If #." t "Remove\\s-+Printing\\s-+If")
+     ("Remove Printing Let" nil "Remove Printing Let #." t "Remove\\s-+Printing\\s-+Let")
      ("Require" nil "Require #." t "Require")
      ("Require Export" nil "Require Export #." t "Require\\s-+Export")
      ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline")
      ("Save" nil "Save." t "Save")
+     ("Search" nil "Search #" nil "Search")
+     ("SearchAbout" nil "SearchAbout #" nil "SearchAbout")
+     ("SearchPattern" nil "SearchPattern #" nil "SearchPattern")
+     ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite")
      ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Extraction\\s-+AutoInline")
      ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Extraction\\s-+Optimize")
      ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Implicit\\s-+Arguments")
@@ -457,6 +468,15 @@ so for the following reasons:
      ("Set Printing Notations" "sprn" "Set Printing Notations" t "Printing\\s-+Notations")
      ("Set Undo" nil "Set Undo #." nil "Undo")
      ("Show" nil "Show #." nil "Show")
+     ("Test" nil "Test" nil "Test" nil t)
+     ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth")
+     ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If")
+     ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let")
+     ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth")
+     ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width")
+     ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard")
+
+
      ("Transparent" nil "Transparent #." nil "Transparent")
      ("Unfocus" nil "Unfocus." nil "Unfocus")
      ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t)