Added a few coq commands.

1 files changed, 7 insertions, 0 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 1722f1bc..470331a6 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -200,6 +200,7 @@ so for the following reasons:
      ("erewrite" "er" "erewrite #" t "erewrite")
      ("eright" "erig" "eright" "eright")
      ("esplit" "esp" "esplit" t "esplit")
+     ("etransitivity" "etr" "etransitivity" t "etransitivity")
      ;;     ("exact" "exa" "exact" t "exact")
      ("exfalso" "exf" "exfalso" t "exfalso")
      ("exists" "ex" "exists #" t "exists")
@@ -257,8 +258,10 @@ so for the following reasons:
      ("quote" "quote" "quote" t "quote")
      ("quote []" "quote2" "quote # [#]" t)
      ("red" "red" "red" t "red")
+     ("rapply" "rap" "rapply #" t "rapply")
      ("refine" "ref" "refine" t "refine")
      ;;      ("reflexivity" "refl" "reflexivity #" t "reflexivity")
+     ("remember" "rem" "remember # as #" t "remember")
      ("rename into" "ren" "rename # into #" t "rename")
      ("replace with" "rep" "replace # with #" t "replace")
      ("replace with in" "repi" "replace # with # in #" t)
@@ -324,6 +327,7 @@ so for the following reasons:
      ("unlock" "unlock" "unlock #" t "unlock")
      ("suffices" "suffices" "suffices # : #" t "suffices")
      ("suff" "suff" "suff # : #" t "suff")
+     ("zify" nil "zify" t "zify")
      )
    coq-user-tactics-db)
   "Coq tactics information list.  See `coq-syntax-db' for syntax."
@@ -505,6 +509,7 @@ so for the following reasons:
     ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t)
     ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t)
     ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure")
+    ("Typeclasses eauto" nil "Typeclasses eauto := #." t "Typeclasses\\s-+eauto")
     ("Variant" "varv" "Variant # : # := # : #." t "Variant")
     )
   "Coq definition keywords information list.  See `coq-syntax-db' for syntax."
@@ -627,6 +632,7 @@ so for the following reasons:
     ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On")
     ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments")
     ("Implicit Types" nil "Implicit Types # : #." t "Implicit\\s-+Types")
+    ("Implicit Type" nil "Implicit Type # : #." t "Implicit\\s-+Type")
     ("Import" nil "Import #." t "Import")
     ("Include" nil "Include #." t "Include")
     ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix")
@@ -651,6 +657,7 @@ so for the following reasons:
     ("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 Hints" nil "Remove Hints #: #." nil "Remove\\s-+Hints")
     ("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")