[nongnu] elpa/proof-general cb23709ad0 4/4: proof-stat: add test for proof-check-annotate

[ELPA Syncer]

branch: elpa/proof-general
commit cb23709ad0c9a9ca0ee48b3ee73c29caea243b98
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>

    proof-stat: add test for proof-check-annotate
---
 ci/simple-tests/Makefile     | 3 +++
 ci/simple-tests/proof_stat.v | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/ci/simple-tests/Makefile b/ci/simple-tests/Makefile
index bda2499fa9..79aec755f8 100644
--- a/ci/simple-tests/Makefile
+++ b/ci/simple-tests/Makefile
@@ -34,8 +34,11 @@ coq-proof-stat-batch-test:
              --eval '(proof-check-report nil "proof_stat.human.gen-out")'
        emacs -batch -l ../../generic/proof-site.el proof_stat.v \
              --eval '(proof-check-report t "proof_stat.tap.gen-out")'
+       emacs -batch -l ../../generic/proof-site.el proof_stat.v \
+             --eval '(proof-check-annotate nil t)'
        cmp proof_stat.human.gen-out proof_stat.human.exp-out && \
                cmp proof_stat.tap.gen-out proof_stat.tap.exp-out && \
+               git diff --exit-code -- proof_stat.v && \
                touch coq-proof-stat-batch-test
 
 .PHONY: clean
diff --git a/ci/simple-tests/proof_stat.v b/ci/simple-tests/proof_stat.v
index 49411eeeb4..c436431b02 100644
--- a/ci/simple-tests/proof_stat.v
+++ b/ci/simple-tests/proof_stat.v
@@ -1,7 +1,7 @@
 
 Definition a : nat := 4.
 
-Lemma a1_equal_4 : a = 2 * 2.
+Lemma a1_equal_4 : a = 2 * 2.                               (* FAIL *)
 Proof using.
   simpl.
   zzzz.                         (* this proof should fail *)
@@ -18,7 +18,7 @@ Proof using.
   trivial.
 Qed.
 
-Lemma b2_equal_6 : b = 2 * 3.
+Lemma b2_equal_6 : b = 2 * 3.                               (* FAIL *)
 Proof using.                    (* this proof should fail *)
 Qed.