diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 68c10abd1..a3701274b 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -558,7 +558,7 @@ so for the following reasons:
     ("Theorem" "th" "Theorem # : #.\n#\nQed." t "Theorem")
     ("Program Theorem" "pth" "Program Theorem # : #.\nProof.\n#\nQed." t "Program\\s-+Theorem")
     ("Obligation" "obl" "Obligation #.\n#\nQed." t "Obligation")
-    ("Obligations" "obls" "Obligations #.\n#\nQed." nil "Obligations")
+    ("Obligations" "obls" "Obligations #.\n#\nQed." t "Obligations")
     ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation")
     )
   "Coq goal starters keywords information list.  See `coq-syntax-db' for syntax."
@@ -573,7 +573,7 @@ so for the following reasons:
      ("About" nil "About #." nil "About")
      ("Check" nil "Check" nil "Check")
      ("Compute" nil "Compute" nil "Compute")
-     ("Fail" nil "Fail" nil "fail")
+     ("Fail" nil "Fail" nil "Fail")
      ("Inspect" nil "Inspect #." nil "Inspect")
      ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File")
      ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library")
@@ -603,40 +603,40 @@ They deserve a separate menu for sending them to Coq without insertion.")
     ("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")
-    ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath")
-    ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path")
+    ("Add LoadPath" nil "Add LoadPath #." t "Add\\s-+LoadPath")
+    ("Add ML Path" nil "Add ML Path #." t "Add\\s-+ML\\s-+Path")
     ("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 Rec LoadPath" nil "Add Rec LoadPath #." t "Add\\s-+Rec\\s-+LoadPath")
+    ("Add Rec ML Path" nil "Add Rec ML Path #." t "Add\\s-+Rec\\s-+ML\\s-+Path")
     ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring")
     ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring")
     ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid")
-    ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations")
+    ("Admit Obligations" "oblsadmit" "Admit Obligations." t "Admit\\s-+Obligations")
     ("Arguments Scope" "argsc" "Arguments Scope @{id} [ @{_} ]" t "Arguments\\s-+Scope")
     ("Local Arguments" nil "Local Arguments @{id} : @{rule}" t "Local\\s-+Arguments")
     ("Arguments" "args" "Arguments @{id} : @{rule}" t "Arguments")
     ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope")
     ("Canonical" nil "Canonical #." t "Canonical")
-    ("Cd" nil "Cd #." nil "Cd")
+    ("Cd" nil "Cd #." t "Cd")
     ("Local Close Scope" "lclsc" "Local Close Scope #" t "Local\\s-+Close\\s-+Scope")
     ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope")
     ("Comments" nil "Comments #." nil "Comments")
-    ("Declare" nil "Declare #." nil "Declare")
+    ("Declare" nil "Declare #." t "Declare")
     ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" )
     ("Eval" nil "Eval #." nil "Eval")
     ("Export" nil "Export #." t "Export")
-    ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant")
-    ("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")
+    ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." t "Extract\\s-+Constant")
+    ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." t "Extract\\s-+Inlined\\s-+Constant")
+    ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." t "Extract")
     ("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")
     ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library")
     ("Extraction" "extr" "Extraction @{id}." nil "Extraction")
-    ("Focus" nil "Focus #." nil "Focus")
+    ("Focus" nil "Focus #." t "Focus")
     ("From" nil "From #." nil "From")
     ("Generalizable Variables" nil "Generalizable Variables #." t "Generalizable\\s-+Variables")
     ("Generalizable All Variables" nil "Generalizable All Variables." t "Generalizable\\s-+All\\s-+Variables")
@@ -659,27 +659,26 @@ They deserve a separate menu for sending them to Coq without insertion.")
     ("Local Notation" "lnots" "Local Notation # := #." t "Local\\s-+Notation")
     ("Local Notation (only parsing)" "lnotsp" "Local Notation # := # (only parsing)." t)
     ("Notation (simple)" "nots" "Notation # := #." t "Notation")
-    ("Typeclasses Opaque" nil "Typeclasses Opaque #." nil "Typeclasses\\s-+Opaque")
-    ("Opaque" nil "Opaque #." nil "Opaque")
+    ("Typeclasses Opaque" nil "Typeclasses Opaque #." t "Typeclasses\\s-+Opaque")
+    ("Opaque" nil "Opaque #." t "Opaque")
     ("Obligation Tactic" nil "Obligation Tactic := #." t "Obligation\\s-+Tactic")
     ("Local Open Scope" nil "Local Open Scope #" t "Local\\s-+Open\\s-+Scope")
     ("Open Local Scope" nil "Open Local Scope #" t "Open\\s-+Local\\s-+Scope")
     ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope")
     ("Preterm" nil "Preterm." nil "Preterm")
-    ("Qed" nil "Qed." nil "Qed")
+    ("Qed" nil "Qed." t "Qed")
     ("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 Hints" nil "Remove Hints #: #." t "Remove\\s-+Hints")
+    ("Remove LoadPath" nil "Remove LoadPath" t "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 Export" nil "Require Export #." t "Require\\s-+Export")
     ("Require Import" nil "Require Import #." t "Require\\s-+Import")
     ("Require" nil "Require #." t "Require")
-    ("Reserved Infix" nil "Reserved Infix" nil "Reserved\\s-+Infix")
-    ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation")
+    ("Reserved Infix" nil "Reserved Infix" t "Reserved\\s-+Infix")
+    ("Reserved Notation" nil "Reserved Notation" t "Reserved\\s-+Notation")
     ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline")
     ("Save" nil "Save." t "Save")
     ("Set Asymmetric Patterns" nil "Set Asymmetric Patterns" t "Set Asymmetric\\s-+Patterns")
@@ -808,9 +807,9 @@ They deserve a separate menu for sending them to Coq without insertion.")
     ("Local Strategy" nil "Local Strategy # [#]." t "Local\\s-+Strategy")
     ("Strategy" nil "Strategy # [#]." t "Strategy")
     ("Tactic Notation" nil "Tactic Notation # := #." t "Tactic\\s-+Notation")
-    ("Transparent" nil "Transparent #." nil "Transparent")
+    ("Transparent" nil "Transparent #." t "Transparent")
 
-    ("Unfocus" nil "Unfocus." nil "Unfocus")
+    ("Unfocus" nil "Unfocus." t "Unfocus")
     ("Unset Asymmetric Patterns" nil "Unset Asymmetric Patterns" t "Unset Asymmetric\\s-+Patterns")
     ("Unset Atomic Load" nil "Unset Atomic Load" t "Unset Atomic\\s-+Load")
     ("Unset Automatic Coercions Import" nil "Unset Automatic Coercions Import" t "Unset Automatic\\s-+Coercions\\s-+Import")