diff --git a/CHANGES b/CHANGES
index b8d846b91..f0dbcf664 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