From 76b586a9823cd0b5a517c11bbc5065a9f1ebfbc5 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Tue, 11 Jun 2024 16:44:30 +0200
Subject: [PATCH 1/4] omit-proofs tests: add new test for bullets and braces

Currently bullets and braces are classified as commands that prevent
proof omission, therefore proofs containing bullets or braces are
never omitted. The new tests is therefore expected to fail.
---
 ci/simple-tests/coq-test-omit-proofs.el | 50 ++++++++++++++++++-------
 ci/simple-tests/omit_test.v             | 24 ++++++++++--
 2 files changed, 56 insertions(+), 18 deletions(-)

diff --git a/ci/simple-tests/coq-test-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el
index ed7aea8d5..68dcf21e3 100644
--- a/ci/simple-tests/coq-test-omit-proofs.el
+++ b/ci/simple-tests/coq-test-omit-proofs.el
@@ -106,7 +106,7 @@ In particular, test that with proof-omit-proofs-option configured:
 
   ;; Check 1: check that the proof is valid and omit can be disabled
   (message "1: check that the proof is valid and omit can be disabled")
-  (should (search-forward "automatic test marker 4" nil t))
+  (should (search-forward "automatic test marker 4 " nil t))
   (forward-line -1)
   ;; simulate C-u prefix argument
   (proof-goto-point '(4))
@@ -140,19 +140,19 @@ In particular, test that with proof-omit-proofs-option configured:
 
   ;; Check 2: check proof-locked-face is active at marker 2 and 3
   (message "2: check proof-locked-face is active at marker 2 and 3")
-  (should (search-backward "automatic test marker 2" nil t))
+  (should (search-backward "automatic test marker 2 " nil t))
   (should (eq (first-overlay-face) 'proof-locked-face))
-  (should (search-forward "automatic test marker 3" nil t))
+  (should (search-forward "automatic test marker 3 " nil t))
   (should (eq (first-overlay-face) 'proof-locked-face))
 
   ;; Check 3: check that the second proof is omitted
   (message "3: check that the second proof is omitted")
   ;; first retract
-  (should (search-backward "automatic test marker 1" nil t))
+  (should (search-backward "automatic test marker 1 " nil t))
   (proof-goto-point)
   (wait-for-coq)
   ;; move forward again
-  (should (search-forward "automatic test marker 4" nil t))
+  (should (search-forward "automatic test marker 4 " nil t))
   (forward-line -1)
   (proof-goto-point)
   (wait-for-coq)
@@ -174,7 +174,7 @@ In particular, test that with proof-omit-proofs-option configured:
 
   ;; Check 4: check proof-omitted-proof-face is active at marker 3
   (message "4: check proof-omitted-proof-face is active at marker 3")
-  (should (search-backward "automatic test marker 3" nil t))
+  (should (search-backward "automatic test marker 3 " nil t))
   ;; debug overlay order
   ;; (mapc
   ;;  (lambda (ov)
@@ -185,9 +185,9 @@ In particular, test that with proof-omit-proofs-option configured:
 
   ;; Check 5: check proof-locked-face is active at marker 1 and 2
   (message "5: check proof-locked-face is active at marker 1 and 2")
-  (should (search-backward "automatic test marker 1" nil t))
+  (should (search-backward "automatic test marker 1 " nil t))
   (should (eq (first-overlay-face) 'proof-locked-face))
-  (should (search-forward "automatic test marker 2" nil t))
+  (should (search-forward "automatic test marker 2 " nil t))
   (should (eq (first-overlay-face) 'proof-locked-face))
 
   ;; Check 6: check that a partial proof at the end is not omitted
@@ -195,7 +195,7 @@ In particular, test that with proof-omit-proofs-option configured:
   (goto-char (point-min))
   (proof-goto-point)
   (wait-for-coq)
-  (should (search-forward "automatic test marker 3" nil t))
+  (should (search-forward "automatic test marker 3 " nil t))
   (forward-line 2)
   (proof-goto-point)
   (wait-for-coq)
@@ -223,11 +223,11 @@ The sources for the test contain a local attribute in form of
   (goto-char (point-min))
   ;; Check that proofs with Hint commands are never omitted
   (message "Check that proofs with Hint commands are never omitted")
-  (should (search-forward "automatic test marker 6" nil t))
+  (should (search-forward "automatic test marker 6 " nil t))
   (forward-line -1)
   (proof-goto-point)
   (wait-for-coq)
-  (should (search-backward "automatic test marker 5" nil t))
+  (should (search-backward "automatic test marker 5 " nil t))
   (should (eq (first-overlay-face) 'proof-locked-face)))
 
 
@@ -245,14 +245,36 @@ This test only checks the faces in the middle of the proof."
   (goto-char (point-min))
   ;; Check that proofs for Let local declarations are never omitted.
   (message "Check that proofs for Let local declarations are never omitted.")
-  (should (search-forward "automatic test marker 8" nil t))
+  (should (search-forward "automatic test marker 8 " nil t))
   (forward-line -1)
   (proof-goto-point)
   (wait-for-coq)
-  (should (search-backward "automatic test marker 7-1" nil t))
+  (should (search-backward "automatic test marker 7-1 " nil t))
   (should (eq (first-overlay-face) 'proof-locked-face))
 
   ;; Check that theorems behind Let definitions are omitted.
   (message "Check that theorems behind Let definitions are omitted.")
-  (should (search-forward "automatic test marker 7-2" nil t))
+  (should (search-forward "automatic test marker 7-2 " nil t))
   (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")
+    (reset-coq)
+    (find-file "omit_test.v")
+    (goto-char (point-min))
+    ;; Check that proofs with bullets and braces are omitted
+    (message "Check that proofs with bullets and braces are omitted")
+    (should (search-forward "automatic test marker 10 " nil t))
+    (setq pos-10 (point))
+    (forward-line 1)
+    (proof-goto-point)
+    (wait-for-coq)
+    (goto-char pos-10)
+    ;; Comment behind should be locked
+    (should (eq (first-overlay-face) 'proof-locked-face))
+    ;; Proof with bullets and braces should be omitted
+    (should (search-backward "automatic test marker 9 " nil t))
+    (should (eq (first-overlay-face) 'proof-omitted-proof-face))))
diff --git a/ci/simple-tests/omit_test.v b/ci/simple-tests/omit_test.v
index 97e43fcd4..7082067bf 100644
--- a/ci/simple-tests/omit_test.v
+++ b/ci/simple-tests/omit_test.v
@@ -8,14 +8,17 @@
  *
  * Lemma never_omit_hints is for test omit-proofs-never-omit-hints: Proofs
  * containing commands should never be skipped (except for a few white-listed
- * commands.
+ * commands).
  *
- * Lemma never_omit_let is for test omit-proofs-never-omit-lets: Proofs of
- * let-theorems should never be omitted.
+ * Lemma never_omit_let and behind_let is for test
+ * omit-proofs-never-omit-lets: Proofs of let-theorems should never be
+ * omitted while proofs behind let declarations should.
  * 
+ * Lemma omit_bullets_and_braces is for test
+ * omit-proofs-omit-bullets-and-braces: Proofs with bullets and braces
+ * should be omitted.
  *)
 
-
 Definition classical_logic : Prop := forall(P : Prop), ~~P -> P.
 
 (* automatic test marker 1 *)
@@ -70,3 +73,16 @@ Proof using.
 Qed.
 
 (* automatic test marker 6 *)
+
+Lemma omit_bullets_and_braces : True /\ (True /\ True).
+Proof using.
+  split.
+  - trivial.
+  - { split.
+      ++ trivial.
+      (* automatic test marker 9 *)
+      ++ trivial.
+    }
+Qed.
+
+(* automatic test marker 10 *)

From 8345dc06230a6f653029843ffe2bb66c0f2c7cc8 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Tue, 11 Jun 2024 15:36:01 +0200
Subject: [PATCH 2/4] omit-proofs: also omit proofs with bullets and braces

---
 ci/simple-tests/coq-test-omit-proofs.el |  1 -
 coq/coq-syntax.el                       | 10 ++++++++++
 coq/coq.el                              |  9 ++++++---
 3 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/ci/simple-tests/coq-test-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el
index 68dcf21e3..20a54b6e8 100644
--- a/ci/simple-tests/coq-test-omit-proofs.el
+++ b/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")
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 03b3f9089..e68bb8f88 100644
--- a/coq/coq-syntax.el
+++ b/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
diff --git a/coq/coq.el b/coq/coq.el
index b48715d55..4d4b5a33e 100644
--- a/coq/coq.el
+++ b/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))))
 

From c2d4771111ee532ee455ed327a6bbcedb28ab099 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Wed, 12 Jun 2024 10:46:16 +0200
Subject: [PATCH 3/4] proof-stat: admitted proofs should count as failing

Proofs terminated with Admitted should count as failing in the
statistics, even when Coq accepts the proofs without error.

The ERT test is marked expected fail, however, this is not possible
for the tests of goal coq-proof-stat-batch-test, therefore the
expected output is wrong, such that these tests succeed.
---
 ci/simple-tests/coq-test-proof-stat.el   | 6 ++++--
 ci/simple-tests/proof_stat.human.exp-out | 3 ++-
 ci/simple-tests/proof_stat.tap.exp-out   | 3 ++-
 ci/simple-tests/proof_stat.v             | 4 ++++
 4 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/ci/simple-tests/coq-test-proof-stat.el b/ci/simple-tests/coq-test-proof-stat.el
index 86470f954..8ec4e25fb 100644
--- a/ci/simple-tests/coq-test-proof-stat.el
+++ b/ci/simple-tests/coq-test-proof-stat.el
@@ -24,6 +24,7 @@ source file."
 
 
 (ert-deftest proof-check-correct-stat ()
+  :expected-result :failed
   "Test `proof-check-report' on a file that is correct in non-opaque parts.
 Test that the report buffer contains the expected output."
   (setq proof-three-window-enable nil)
@@ -39,14 +40,15 @@ Test that the report buffer contains the expected output."
     ;; the summary should be correct
     (goto-char (point-min))
     (should
-     (search-forward "3 opaque proofs recognized: 1 successful 2 FAILING"
+     (search-forward "4 opaque proofs recognized: 2 successful 2 FAILING"
                      nil t))
     ;; results for all 3 test lemmas should be correct
     (mapc
      (lambda (s) (should (search-forward s nil t)))
      '("FAIL a1_equal_4"
        "OK   b_equal_6"
-       "FAIL b2_equal_6"))))
+       "FAIL b2_equal_6"
+       "FAIL use_admit"))))
 
 
 (ert-deftest proof-check-error-on-error ()
diff --git a/ci/simple-tests/proof_stat.human.exp-out b/ci/simple-tests/proof_stat.human.exp-out
index 82346b541..901c8b382 100644
--- a/ci/simple-tests/proof_stat.human.exp-out
+++ b/ci/simple-tests/proof_stat.human.exp-out
@@ -1,9 +1,10 @@
 Proof check results for proof_stat.v
 
-3 opaque proofs recognized: 1 successful 2 FAILING
+4 opaque proofs recognized: 2 successful 2 FAILING
 
   FAIL a1_equal_4
   OK   b_equal_6
   FAIL b2_equal_6
+  OK   use_admit
 
 
diff --git a/ci/simple-tests/proof_stat.tap.exp-out b/ci/simple-tests/proof_stat.tap.exp-out
index 7903afc6a..1735d29f7 100644
--- a/ci/simple-tests/proof_stat.tap.exp-out
+++ b/ci/simple-tests/proof_stat.tap.exp-out
@@ -1,7 +1,8 @@
 TAP version 13
-1..3
+1..4
 not ok 1 a1_equal_4
 ok 2 b_equal_6
 not ok 3 b2_equal_6
+ok 4 use_admit
 
 
diff --git a/ci/simple-tests/proof_stat.v b/ci/simple-tests/proof_stat.v
index c436431b0..415b18bc2 100644
--- a/ci/simple-tests/proof_stat.v
+++ b/ci/simple-tests/proof_stat.v
@@ -22,3 +22,7 @@ Lemma b2_equal_6 : b = 2 * 3.                               (* FAIL *)
 Proof using.                    (* this proof should fail *)
 Qed.
 
+Lemma use_admit : 0 = 1.
+Proof using.               (* this proof succeeds but should count as failing *)
+  admit.
+Admitted.

From b5241e86d226505d8b42214d28e54a01565dd763 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Wed, 12 Jun 2024 11:27:09 +0200
Subject: [PATCH 4/4] proof-stat: admitted proofs count as failing

Change `proof-check-chunks' such that Admitted proofs are reported as
failing.
---
 ci/simple-tests/proof_stat.human.exp-out |  4 ++--
 ci/simple-tests/proof_stat.tap.exp-out   |  2 +-
 ci/simple-tests/proof_stat.v             |  2 +-
 coq/coq-syntax.el                        |  6 ++++++
 coq/coq.el                               |  3 ++-
 doc/PG-adapting.texi                     | 20 +++++++++++++++++---
 doc/ProofGeneral.texi                    | 20 ++++++++++++--------
 generic/pg-user.el                       | 21 +++++++++++++++++----
 generic/proof-config.el                  | 11 +++++++++++
 9 files changed, 69 insertions(+), 20 deletions(-)

diff --git a/ci/simple-tests/proof_stat.human.exp-out b/ci/simple-tests/proof_stat.human.exp-out
index 901c8b382..472312ed8 100644
--- a/ci/simple-tests/proof_stat.human.exp-out
+++ b/ci/simple-tests/proof_stat.human.exp-out
@@ -1,10 +1,10 @@
 Proof check results for proof_stat.v
 
-4 opaque proofs recognized: 2 successful 2 FAILING
+4 opaque proofs recognized: 1 successful 3 FAILING
 
   FAIL a1_equal_4
   OK   b_equal_6
   FAIL b2_equal_6
-  OK   use_admit
+  FAIL use_admit
 
 
diff --git a/ci/simple-tests/proof_stat.tap.exp-out b/ci/simple-tests/proof_stat.tap.exp-out
index 1735d29f7..86bd533ba 100644
--- a/ci/simple-tests/proof_stat.tap.exp-out
+++ b/ci/simple-tests/proof_stat.tap.exp-out
@@ -3,6 +3,6 @@ TAP version 13
 not ok 1 a1_equal_4
 ok 2 b_equal_6
 not ok 3 b2_equal_6
-ok 4 use_admit
+not ok 4 use_admit
 
 
diff --git a/ci/simple-tests/proof_stat.v b/ci/simple-tests/proof_stat.v
index 415b18bc2..ffdccda66 100644
--- a/ci/simple-tests/proof_stat.v
+++ b/ci/simple-tests/proof_stat.v
@@ -22,7 +22,7 @@ Lemma b2_equal_6 : b = 2 * 3.                               (* FAIL *)
 Proof using.                    (* this proof should fail *)
 Qed.
 
-Lemma use_admit : 0 = 1.
+Lemma use_admit : 0 = 1.                                    (* FAIL *)
 Proof using.               (* this proof succeeds but should count as failing *)
   admit.
 Admitted.
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index e68bb8f88..fbb5398f9 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1136,6 +1136,12 @@ different."
   :type 'string
   :group 'coq)
 
+(defcustom coq-omit-cheating-regexp "Admitted"
+  "Value for `proof-omit-cheating-regexp'.
+Very similar to `coq-omit-proof-admit-command', but without the dot."
+  :type 'regexp
+  :group 'coq)
+
 ;; ----- keywords for font-lock.
 
 (defvar coq-keywords-kill-goal
diff --git a/coq/coq.el b/coq/coq.el
index 4d4b5a33e..fdafe2dd4 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1964,7 +1964,8 @@ at `proof-assistant-settings-cmds' evaluation time.")
    proof-script-definition-end-regexp coq-definition-end-regexp
    proof-script-proof-admit-command coq-omit-proof-admit-command
    proof-script-cmd-prevents-proof-omission #'coq-cmd-prevents-proof-omission
-   proof-script-cmd-force-next-proof-kept coq-cmd-force-next-proof-kept)
+   proof-script-cmd-force-next-proof-kept coq-cmd-force-next-proof-kept
+   proof-omit-cheating-regexp coq-omit-cheating-regexp)
 
   ;; proof-check-report/proof-check-annotate config
   (setq
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index d63478a38..865a3083d 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -1289,9 +1289,12 @@ The other material is asserted in the usual way and
 opaque proofs it first tries to assert them in the usual way too. If
 this succeeds the proof is considered valid. Otherwise the proof is
 replaced with @code{proof-script-proof-admit-command} and the proof is
-considered invalid. To associate theorem names with opaque proofs, the
-function @code{proof-get-proof-info-fn} is called, which is identical
-to @code{proof-tree-get-proof-info}, @xref{Proof Tree Elisp
+considered invalid. In order to consider Admitted proofs as invalid
+ones, proofs whose last command matches
+@code{proof-omit-cheating-regexp} count as invalid. To associate
+theorem names with opaque proofs, the function
+@code{proof-get-proof-info-fn} is called, which is identical to
+@code{proof-tree-get-proof-info}, @xref{Proof Tree Elisp
 configuration}.
 
 To enable proof status statistics, the omit-proofs feature must be
@@ -1328,6 +1331,17 @@ This function takes a state as argument as returned by
 the proof assistant back to the same state.
 @end defvar
 
+@c TEXI DOCSTRING MAGIC: proof-omit-cheating-regexp
+@defvar proof-omit-cheating-regexp 
+Regular expression matching proof closing commands for incomplete proofs.@*
+If set, this regular expression is applied to the last command of
+opaque proofs. If it matches the proofs counts as invalid for the
+proof-status statistics and annotation feature. For Coq this is
+used to mark Admitted proofs as invalid.
+
+This option can be left at @samp{nil}.
+@end defvar
+
 
 @node Safe (state-preserving) commands
 @section Safe (state-preserving) commands
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index e5aaeb23d..acaed3617 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2267,7 +2267,8 @@ in the current buffer, i.e., it generates an overview that shows which
 of the opaque proofs in the current buffer are currently valid and
 which are failing. When used interactively, the proof status is shown
 in the buffer @code{*proof-check-report*} (as long as
-@code{proof-check-report-buffer} is not changed).
+@code{proof-check-report-buffer} is not changed). Note that incomplete
+proofs, i.e., Admitted proofs for Coq, count as invalid.
 
 The command @code{proof-check-annotate} (menu @code{Proof-General ->
 Annotate Failing Proofs}) modifies the current buffer and places
@@ -2285,7 +2286,10 @@ only work for Coq.
 Generate an overview about valid and invalid proofs.@*
 This command completely processes the current buffer and
 generates an overview about all the opaque proofs in it and
-whether their proof scripts are valid or invalid.
+whether their proof scripts are valid or invalid. Note that
+proofs closed with a cheating command (see
+@samp{@code{proof-omit-cheating-regexp}}), i.e., Admitted for Coq, count as
+invalid.
 
 This command makes sense for a development process where invalid
 proofs are permitted and vos compilation and the omit proofs
@@ -5318,12 +5322,12 @@ The command @code{proof-check-report} (menu @code{Proof-General ->
 Check Opaque Proofs}) generates the proof status of all opaque proofs
 in the current buffer, i.e., it generates an overview that shows which
 of the opaque proofs in the current buffer are currently valid and
-which are failing. This command is useful for a development process
-where invalid proofs are permitted and vos compilation (@xref{Quick
-and inconsistent compilation}) and the omit proofs feature
-(@xref{Omitting proofs for speed}) are used to work at the most
-interesting or challenging point instead of on the first invalid
-proof.
+which are failing, where Admitted proofs count as failing. This
+command is useful for a development process where invalid proofs are
+permitted and vos compilation (@xref{Quick and inconsistent
+compilation}) and the omit proofs feature (@xref{Omitting proofs for
+speed}) are used to work at the most interesting or challenging point
+instead of on the first invalid proof.
 
 The command @code{proof-check-annotate} (menu @code{Proof-General ->
 Annotate Failing Proofs}) can then be used to consistently annotate
diff --git a/generic/pg-user.el b/generic/pg-user.el
index ed86fc062..07ff560fb 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -735,7 +735,9 @@ errors are silently replaced by
 `proof-script-proof-admit-command'. The result is a list of proof
 status results, one for each 'proof chunk in the same order. Each
 proof-status result is a list of 4 elements as follows.
-- 1st: proof status as `t' or `nil'.
+- 1st: proof status as `t' or `nil'. Proofs closed with a match
+  of `proof-omit-cheating-regexp', if defined, count as failing,
+  i.e., their status is `nil'.
 - 2nd: the name of the proof as reported by
   `proof-get-proof-info-fn'.
 - 3rd: Position of the start of the span containing the theorem
@@ -762,7 +764,8 @@ proof-status result is a list of 4 elements as follows.
                                   (nth 2 last-item)
                                   (cons 'empty-action-list (nth 3 last-item))))
              (vanillas-rev-updated (cons new-last-item (cdr vanillas-rev)))
-             error)
+             error
+             cheated)
         ;; if this is a proof chunk the next must be no-proof or must not exist
         (cl-assert (or (not (eq this-mode 'proof))
                        (or (eq next-mode 'no-proof) (eq next-mode nil)))
@@ -813,8 +816,15 @@ proof-status result is a list of 4 elements as follows.
             (proof-set-locked-end last-span-end)
             (cl-assert (not (cadr (funcall proof-get-proof-info-fn)))
                        nil "proof-check: still in proof after admitting"))
+          (when (and proof-omit-cheating-regexp
+                     ;; check if somebody cheated - cheated proofs
+                     ;; should count as failing
+                     (proof-string-match
+                      proof-omit-cheating-regexp
+                      (mapconcat #'identity (nth 1 last-item) " ")))
+            (setq cheated t))
           (push
-           (cons (not error)
+           (cons (not (or error cheated))
                  (cons (cadr current-proof-state-and-name) proof-start-points))
            proof-results)))
         
@@ -863,7 +873,10 @@ This function does not (re-)compile required files."
   "Generate an overview about valid and invalid proofs.
 This command completely processes the current buffer and
 generates an overview about all the opaque proofs in it and
-whether their proof scripts are valid or invalid.
+whether their proof scripts are valid or invalid. Note that
+proofs closed with a cheating command (see
+`proof-omit-cheating-regexp'), i.e., Admitted for Coq, count as
+invalid.
 
 This command makes sense for a development process where invalid
 proofs are permitted and vos compilation and the omit proofs
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 1c5ede807..aa79b85c4 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -738,6 +738,17 @@ without surrounding space."
   :type 'boolean
   :group 'proof-script)
 
+(defcustom proof-omit-cheating-regexp nil
+  "Regular expression matching proof closing commands for incomplete proofs.
+If set, this regular expression is applied to the last command of
+opaque proofs. If it matches the proofs counts as invalid for the
+proof-status statistics and annotation feature. For Coq this is
+used to mark Admitted proofs as invalid.
+
+This option can be left at `nil'."
+  :type 'regexp
+  :group 'proof-script)
+
 ;; proof-omit-proofs-option is in proof-useropts as user option
 
 (defcustom proof-script-proof-start-regexp nil