Fixing track 414 by adding Preterm as a state preserving command.

1 files changed, 3 insertions, 1 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index eb04e901..14979876 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -481,6 +481,7 @@ See also `coq-prog-env' to adjust the environment."
     ("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")
     ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation")
     )
   "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. "
@@ -558,6 +559,7 @@ See also `coq-prog-env' to adjust the environment."
      ("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")
      ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions")
      ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint)
      ("Print" "p" "Print #." nil "Print")
@@ -592,7 +594,7 @@ See also `coq-prog-env' to adjust the environment."
      ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations")
      ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo")
      ("Show" nil "Show #." nil "Show")
-     ("Solve Obligations" "oblssolve" "Solve Obligations using #." nil "Solve\\s-+Obligations")
+     ("Solve Obligations" "oblssolve" "Solve Obligations using #." t "Solve\\s-+Obligations")
      ("Tactic Notation" nil "Tactic Notation # := #." t "Tactic\\s-+Notation")
      ("Test" nil "Test" nil "Test" nil t)
      ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth")