branch: elpa/proof-general
commit 85de7aa1874cd0bc1e15b85bb156f2ee879ad44a
Author: Hendrik Tews <hend...@askra.de>
Commit: hendriktews <hend...@askra.de>
proof-stat: add CHANGES entry
---
CHANGES | 27 ++++++++++++++++++---------
1 file changed, 18 insertions(+), 9 deletions(-)
diff --git a/CHANGES b/CHANGES
index b8d846b91f..f0dbcf6649 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,6 +14,9 @@ the Git ChangeLog, the GitHub repo
https://github.com/ProofGeneral/PG
Proof-tree visualization is currently only supported for Coq. The
prooftree support has been substantially rewritten, making use of
the much better support since Coq version 8.11.
+*** New command `proof-check-proofs' to generates the proof status
+ of all opaque proofs. Currently only available for Coq, see Coq
+ changes below for more details.
** Coq changes
*** support Coq 8.19
@@ -23,15 +26,21 @@ the Git ChangeLog, the GitHub repo
https://github.com/ProofGeneral/PG
modules as coqdep error.
*** Renew support for proof-tree visualization, see description in
generic changes above.
-
-
-**** New options coq-compile-extra-coqc-arguments and
- coq-compile-extra-coqdep-arguments to configure additional
- command line arguments to calls of, respetively, coqc and coqdep
- during auto compilation.
-
-**** Fix issues #687 and #688 where the omit-proofs feature causes
- errors on correct code.
+*** New command `proof-check-proofs' to generates the proof status
+ of all opaque proofs. This command is useful for a development
+ process where invalid proofs are permitted and vos compilation and
+ the omit proofs feature are used to work at the most interesting
+ or challenging point instead of on the first invalid proof. The
+ command generates a list of all opaque proofs in the current
+ buffer together with the information whether the proof script is
+ currently valid or invalid. The command can also be run in batch
+ mode, for instance in a continuous integration environment.
+*** New options coq-compile-extra-coqc-arguments and
+ coq-compile-extra-coqdep-arguments to configure additional
+ command line arguments to calls of, respetively, coqc and coqdep
+ during auto compilation.
+*** Fix issues #687 and #688 where the omit-proofs feature causes
+ errors on correct code.
* Changes of Proof General 4.5 from Proof General 4.4
