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

@@ -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 ()

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
 
 

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
 
 

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.