From 6c5c3bd20b846122b773ab52f1bd46674cadc069 Mon Sep 17 00:00:00 2001
From: Hendrik Tews <hendrik@askra.de>
Date: Mon, 29 Apr 2024 17:23:35 +0200
Subject: [PATCH] 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 bda2499fa..79aec755f 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 49411eeeb..c436431b0 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.