omit-proofs: also omit proofs with bullets and braces

ci/simple-tests/coq-test-omit-proofs.el

@@ -258,7 +258,6 @@ This test only checks the faces in the middle of the proof."
   (should (eq (first-overlay-face) 'proof-omitted-proof-face)))
 
 (ert-deftest omit-proofs-omit-bullets-and-braces ()
-  :expected-result :failed
   (let ((proof-omit-proofs-option t)
         pos-10)
     (message "omit-proofs-omit-bullets-and-braces: Check bullets and braces")

coq/coq-syntax.el

@@ -1433,6 +1433,16 @@ different."
 Used in `coq-cmd-prevents-proof-omission' to identify tactics
 that only have proof-local effects.")
 
+(defconst coq-bullet-regexp "^\\(-+\\|\\++\\|\\*+\\)$"
+  "Regular expression matching bullets.
+Used in `coq-cmd-prevents-proof-omission' to identify tactics
+that only have proof-local effects.")
+
+(defconst coq-braces-regexp "^\\({\\|}\\)$"
+  "Regular expression matching braces used for focussing and unfocussing.
+Used in `coq-cmd-prevents-proof-omission' to identify tactics
+that only have proof-local effects.")
+
 (defcustom coq-cmd-force-next-proof-kept "Let"
   "Instantiating for `proof-script-cmd-force-next-proof-kept'.
 Regular expression for commands that prevent omitting the next

coq/coq.el

@@ -745,9 +745,12 @@ have effects outside the proof, which would prohibit omitting the
 proof, see `proof-script-omit-proofs'.
 
 Commands starting lower case are deemed as tactics that have
-proof local effect only. Everything else is checked against the
-STATECH field in the coq syntax data base, see coq-db.el."
-  (if (proof-string-match coq-lowercase-command-regexp cmd)
+proof local effect only and so are bullets and braces. Everything
+else is checked against the STATECH field in the coq syntax data
+base, see coq-db.el."
+  (if (or (proof-string-match coq-lowercase-command-regexp cmd)
+          (proof-string-match coq-bullet-regexp cmd)
+          (proof-string-match coq-braces-regexp cmd))
       nil
     (not (coq-state-preserving-p cmd))))