diff --git a/doc/master/adaptingman/Beginning-with-a-New-Prover.html b/doc/master/adaptingman/Beginning-with-a-New-Prover.html
index 3a5a943..220372e 100644
--- a/doc/master/adaptingman/Beginning-with-a-New-Prover.html
+++ b/doc/master/adaptingman/Beginning-with-a-New-Prover.html
@@ -258,7 +258,7 @@ <h2 class="section">1.3 Major modes used by Proof General</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Concept-Index.html b/doc/master/adaptingman/Concept-Index.html
index 5f14fed..4d4396f 100644
--- a/doc/master/adaptingman/Concept-Index.html
+++ b/doc/master/adaptingman/Concept-Index.html
@@ -141,7 +141,7 @@ <h1 class="unnumbered">Concept Index</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Configuring-Editing-Syntax.html b/doc/master/adaptingman/Configuring-Editing-Syntax.html
index a22e8a4..f2850dd 100644
--- a/doc/master/adaptingman/Configuring-Editing-Syntax.html
+++ b/doc/master/adaptingman/Configuring-Editing-Syntax.html
@@ -86,7 +86,7 @@ <h1 class="chapter">9. Configuring Editing Syntax</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Configuring-Font-Lock.html b/doc/master/adaptingman/Configuring-Font-Lock.html
index 44879ca..049ffef 100644
--- a/doc/master/adaptingman/Configuring-Font-Lock.html
+++ b/doc/master/adaptingman/Configuring-Font-Lock.html
@@ -104,7 +104,7 @@ <h1 class="chapter">10. Configuring Font Lock</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization.html b/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization.html
index 9b48764..2f868bf 100644
--- a/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization.html
+++ b/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization.html
@@ -455,7 +455,7 @@ <h3 class="subsection">12.4.2 Prooftree Adaption</h3>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Configuring-Tokens.html b/doc/master/adaptingman/Configuring-Tokens.html
index 0a86b92..c75280a 100644
--- a/doc/master/adaptingman/Configuring-Tokens.html
+++ b/doc/master/adaptingman/Configuring-Tokens.html
@@ -78,7 +78,7 @@ <h1 class="chapter">11. Configuring Tokens</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Demonstration-Instantiations.html b/doc/master/adaptingman/Demonstration-Instantiations.html
index afaa5e5..b6df200 100644
--- a/doc/master/adaptingman/Demonstration-Instantiations.html
+++ b/doc/master/adaptingman/Demonstration-Instantiations.html
@@ -261,7 +261,7 @@ <h2 class="section">B.2 demoisa.el</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Function-Index.html b/doc/master/adaptingman/Function-Index.html
index 25f0e6a..7c4ea49 100644
--- a/doc/master/adaptingman/Function-Index.html
+++ b/doc/master/adaptingman/Function-Index.html
@@ -104,7 +104,7 @@ <h1 class="unnumbered">Function and Command Index</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Global-Constants.html b/doc/master/adaptingman/Global-Constants.html
index c178905..73bd384 100644
--- a/doc/master/adaptingman/Global-Constants.html
+++ b/doc/master/adaptingman/Global-Constants.html
@@ -55,7 +55,7 @@ <h1 class="chapter">7. Global Constants</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Goals-Buffer-Settings.html b/doc/master/adaptingman/Goals-Buffer-Settings.html
index f42752f..5b4733d 100644
--- a/doc/master/adaptingman/Goals-Buffer-Settings.html
+++ b/doc/master/adaptingman/Goals-Buffer-Settings.html
@@ -102,7 +102,7 @@ <h1 class="chapter">5. Goals Buffer Settings</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Handling-Multiple-Files.html b/doc/master/adaptingman/Handling-Multiple-Files.html
index 6f8a54a..6e583c5 100644
--- a/doc/master/adaptingman/Handling-Multiple-Files.html
+++ b/doc/master/adaptingman/Handling-Multiple-Files.html
@@ -190,7 +190,7 @@ <h1 class="chapter">8. Handling Multiple Files</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Internals-of-Proof-General.html b/doc/master/adaptingman/Internals-of-Proof-General.html
index f7690ce..f5d0e60 100644
--- a/doc/master/adaptingman/Internals-of-Proof-General.html
+++ b/doc/master/adaptingman/Internals-of-Proof-General.html
@@ -1256,7 +1256,7 @@ <h2 class="section">14.7 Debugging</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Introduction.html b/doc/master/adaptingman/Introduction.html
index 7fb097d..9edebfa 100644
--- a/doc/master/adaptingman/Introduction.html
+++ b/doc/master/adaptingman/Introduction.html
@@ -121,7 +121,7 @@ <h2 class="unnumberedsec">Credits</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Menus-and-Toolbar-and-User_002dlevel-Commands.html b/doc/master/adaptingman/Menus-and-Toolbar-and-User_002dlevel-Commands.html
index eb949f0..e97f350 100644
--- a/doc/master/adaptingman/Menus-and-Toolbar-and-User_002dlevel-Commands.html
+++ b/doc/master/adaptingman/Menus-and-Toolbar-and-User_002dlevel-Commands.html
@@ -179,7 +179,7 @@ <h2 class="section">2.3 Toolbar configuration</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/PG-adapting_abt.html b/doc/master/adaptingman/PG-adapting_abt.html
index 85b6ff4..06f1997 100644
--- a/doc/master/adaptingman/PG-adapting_abt.html
+++ b/doc/master/adaptingman/PG-adapting_abt.html
@@ -14,7 +14,7 @@
 </div>
 <h1>About This Document</h1>
 <p>
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
 </p>
 <p>
   The buttons in the navigation panels have the following meaning:
@@ -124,7 +124,7 @@ <h1>About This Document</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/PG-adapting_toc.html b/doc/master/adaptingman/PG-adapting_toc.html
index df4ad56..a454cd7 100644
--- a/doc/master/adaptingman/PG-adapting_toc.html
+++ b/doc/master/adaptingman/PG-adapting_toc.html
@@ -130,7 +130,7 @@ <h1>Table of Contents</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Plans-and-Ideas.html b/doc/master/adaptingman/Plans-and-Ideas.html
index a7e3cfe..3ac09a7 100644
--- a/doc/master/adaptingman/Plans-and-Ideas.html
+++ b/doc/master/adaptingman/Plans-and-Ideas.html
@@ -167,7 +167,7 @@ <h2 class="section">A.3 Browser mode for script files and theories</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Proof-Script-Settings.html b/doc/master/adaptingman/Proof-Script-Settings.html
index 1eb36b1..160694c 100644
--- a/doc/master/adaptingman/Proof-Script-Settings.html
+++ b/doc/master/adaptingman/Proof-Script-Settings.html
@@ -686,17 +686,18 @@ <h2 class="section">3.6 Omitting proofs for speed</h2>
 <a class="anchor" id="Proof-status-statistic-1"></a>
 <h2 class="section">3.7 Proof status statistic</h2>
 
-<p>The command <code>proof-check-proofs</code> builds on the omit-proofs
-feature. Using its machinery, it splits the current buffer into opaque
-proofs and all other material. The other material is asserted in the
-usual way and <code>proof-check-proofs</code> aborts if it detects an error
-in there. For opaque proofs the command first tries to assert them in
-the usual way too. If this succeeds the proof is considered valid.
-Otherwise the proof is replaced with
-<code>proof-script-proof-admit-command</code> and the proof is considered
-invalid. To associate theorem names with opaque proofs, the function
-<code>proof-get-proof-info-fn</code> is called, which is identical to
-<code>proof-tree-get-proof-info</code>, See section <a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#Proof-Tree-Elisp-configuration">Proof Tree Elisp configuration</a>.
+<p>The commands <code>proof-check-report</code> and <code>proof-check-annotate</code>
+build on the omit-proofs feature. Using its machinery,
+<code>proof-check-proofs</code>, the inner working horse of both commands,
+splits the current buffer into opaque proofs and all other material.
+The other material is asserted in the usual way and
+<code>proof-check-proofs</code> aborts if it detects an error in there. For
+opaque proofs it first tries to assert them in the usual way too. If
+this succeeds the proof is considered valid. Otherwise the proof is
+replaced with <code>proof-script-proof-admit-command</code> and the proof is
+considered invalid. To associate theorem names with opaque proofs, the
+function <code>proof-get-proof-info-fn</code> is called, which is identical
+to <code>proof-tree-get-proof-info</code>, See section <a href="/doc/master/adaptingman/Configuring-Proof_002dTree-Visualization#Proof-Tree-Elisp-configuration">Proof Tree Elisp configuration</a>.
 </p>
 <p>To enable proof status statistics, the omit-proofs feature must be
 configured, See section <a href="#Omitting-proofs-for-speed">Omitting proofs for speed</a>. Additionally, the
@@ -898,7 +899,7 @@ <h2 class="section">3.12 Completions</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Proof-Shell-Settings.html b/doc/master/adaptingman/Proof-Shell-Settings.html
index 57adf98..dd4cbc1 100644
--- a/doc/master/adaptingman/Proof-Shell-Settings.html
+++ b/doc/master/adaptingman/Proof-Shell-Settings.html
@@ -748,7 +748,7 @@ <h2 class="section">4.5 Hooks and other settings</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Splash-Screen-Settings.html b/doc/master/adaptingman/Splash-Screen-Settings.html
index 78ce668..2e72e99 100644
--- a/doc/master/adaptingman/Splash-Screen-Settings.html
+++ b/doc/master/adaptingman/Splash-Screen-Settings.html
@@ -55,7 +55,7 @@ <h1 class="chapter">6. Splash Screen Settings</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Variable-Index.html b/doc/master/adaptingman/Variable-Index.html
index ca6934c..f6c5d14 100644
--- a/doc/master/adaptingman/Variable-Index.html
+++ b/doc/master/adaptingman/Variable-Index.html
@@ -235,7 +235,7 @@ <h1 class="unnumbered">Variable and User Option Index</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/Writing-More-Lisp-Code.html b/doc/master/adaptingman/Writing-More-Lisp-Code.html
index cde6a97..b5dbb22 100644
--- a/doc/master/adaptingman/Writing-More-Lisp-Code.html
+++ b/doc/master/adaptingman/Writing-More-Lisp-Code.html
@@ -248,7 +248,7 @@ <h2 class="section">13.4 Useful functions and macros</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/adaptingman/index.html b/doc/master/adaptingman/index.html
index 8375cf1..4b09d7c 100644
--- a/doc/master/adaptingman/index.html
+++ b/doc/master/adaptingman/index.html
@@ -80,7 +80,7 @@ <h1 class="settitle">Proof General</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Advanced-Script-Management-and-Editing.html b/doc/master/userman/Advanced-Script-Management-and-Editing.html
index c28bbe4..61cf53f 100644
--- a/doc/master/userman/Advanced-Script-Management-and-Editing.html
+++ b/doc/master/userman/Advanced-Script-Management-and-Editing.html
@@ -389,7 +389,7 @@ <h2 class="section">3.7 Asserting across files</h2>
 <h2 class="section">3.8 Proof status statistic</h2>
 <a class="anchor" id="index-Proof-status-statistic"></a>
 
-<p>The command <code>proof-check-proofs</code> (menu <code>Proof-General -&gt;
+<p>The command <code>proof-check-report</code> (menu <code>Proof-General -&gt;
 Check Opaque Proofs</code>) generates the proof status of all opaque proofs
 in the current buffer, i.e., it generates an overview that shows which
 of the opaque proofs in the current buffer are currently valid and
@@ -397,10 +397,19 @@ <h2 class="section">3.8 Proof status statistic</h2>
 in the buffer <code>*proof-check-report*</code> (as long as
 <code>proof-check-report-buffer</code> is not changed).
 </p>
-<p>Currently <code>proof-check-proofs</code> does only work for Coq.
+<p>The command <code>proof-check-annotate</code> (menu <code>Proof-General -&gt;
+Annotate Failing Proofs</code>) modifies the current buffer and places
+comments containing <code>FAIL</code> on all failing opaque proofs. With
+prefix argument also the passing proofs are annotated with
+<code>PASS</code>. For configuring the position of these comments, see
+<code>proof-check-annotate-position</code> and
+<code>proof-check-annotate-right-margin</code>.
+</p>
+<p>Currently <code>proof-check-report</code> and <code>proof-check-annotate</code>
+only work for Coq.
 </p>
 <dl>
-<dt><a class="anchor" id="index-proof_002dcheck_002dproofs"></a><u>Command:</u> <b>proof-check-proofs</b><i> tap &amp;optional batch</i></dt>
+<dt><a class="anchor" id="index-proof_002dcheck_002dreport"></a><u>Command:</u> <b>proof-check-report</b><i> tap &amp;optional batch</i></dt>
 <dd><p>Generate an overview about valid and invalid proofs.<br>
 This command completely processes the current buffer and
 generates an overview about all the opaque proofs in it and
@@ -418,45 +427,97 @@ <h2 class="section">3.8 Proof status statistic</h2>
 protocol (<var>tap</var>). Argument <var>batch</var> controls where the overview goes
 to. If nil, or in an interactive call, the overview appears in
 &lsquo;<samp><code>proof-check-report-buffer</code></samp>&rsquo;. If <var>batch</var> is a string, it should be a
-filename and the overview is appended there. Otherwise the
-overview is output via &lsquo;<samp>message</samp>&rsquo; such that it appears on stdout
-when this command runs in batch mode.
+filename to write the overview to. Otherwise the overview is
+output via &lsquo;<samp>message</samp>&rsquo; such that it appears on stdout when this
+command runs in batch mode.
 </p>
 <p>In the same way as the omit-proofs feature, this command only
 tolerates errors inside scripts of opaque proofs. Any other error
 is reported to the user without generating an overview. The
-overview only contains those names of theorems whose proofs
+overview only contains those names of theorems whose proof
 scripts are classified as opaque by the omit-proofs feature. For
 Coq for instance, among others, proof scripts terminated with
 <code>'Defined'</code> are not opaque and do not appear in the generated
 overview.
 </p>
 <p>Note that this command does not (re-)compile required files.
-Files must be required before running this commands, for instance
-by asserting all require commands beforehand.
+Dependencies must be compiled before running this commands, for
+instance by asserting all require commands beforehand.
+</p></dd></dl>
+
+<dl>
+<dt><a class="anchor" id="index-proof_002dcheck_002dannotate"></a><u>Command:</u> <b>proof-check-annotate</b><i> annotate-passing &amp;optional save-buffer</i></dt>
+<dd><p>Annotate failing proofs in current buffer with a &quot;<var>fail</var>&quot; comment.<br>
+This function modifies the current buffer in place. Use with
+care!
+</p>
+<p>Similarly to &lsquo;<samp><code>proof-check-report</code></samp>&rsquo;, check all opaque proofs in the
+current buffer. Instead of generating a report, failing proofs
+are annotated with &quot;<var>fail</var>&quot; in a comment. Existing &quot;<var>pass</var>&quot; or
+&quot;<var>fail</var>&quot; comments (e.g., from a previous run) are deleted
+together with the surrounding white space. With prefix argument
+(or when <var>annotate-passing</var> is non-nil) also passing proofs are
+annotated with a &quot;<var>pass</var>&quot; comment. Pass and fail comments can be
+placed at the last or second last statement before the opaque
+proof. For Coq this corresponds to the proof using and the
+theorem statement, respectively. In both cases the comment is
+placed at the right margin of the first line, see
+&lsquo;<samp><code>proof-check-annotate-position</code></samp>&rsquo; and
+&lsquo;<samp><code>proof-check-annotate-right-margin</code></samp>&rsquo;.
+</p>
+<p>Interactively, this command does not save the current buffer
+after placing the annotations. With <var>save-buffer</var> non-nil, the
+current buffer is saved if it has been modified.
+</p></dd></dl>
+
+<dl>
+<dt><a class="anchor" id="index-proof_002dcheck_002dannotate_002dposition"></a><u>Variable:</u> <b>proof-check-annotate-position</b></dt>
+<dd><p>Line for annotating proofs with &quot;<var>pass</var>&quot; or &quot;<var>fail</var>&quot; comments.<br>
+This option determines the line where &lsquo;<samp><code>proof-check-annotate</code></samp>&rsquo; puts
+comments with &quot;<var>pass</var>&quot; and &quot;<var>fail</var>&quot;. Value &lsquo;&rsquo;theoren&rsquo; uses the
+first line of the second last statement before the start of the
+opaque proof, which corresponds to the line containing a Theorem
+keyword for Coq. Value &lsquo;&rsquo;proof-using&rsquo; uses the first line of the
+last statement before the opaque proof, which corresponds to the
+Proof using line for Coq.
+</p></dd></dl>
+
+<dl>
+<dt><a class="anchor" id="index-proof_002dcheck_002dannotate_002dright_002dmargin"></a><u>Variable:</u> <b>proof-check-annotate-right-margin</b></dt>
+<dd><p>Right margin for &quot;<var>pass</var>&quot; and &quot;<var>fail</var>&quot; comments.<br>
+This option determines the right margin to which
+&lsquo;<samp><code>proof-check-annotate</code></samp>&rsquo; right-aligns the comments with &quot;<var>pass</var>&quot;
+and &quot;<var>fail</var>&quot;. If nil, the value of &lsquo;<samp><code>fill-column</code></samp>&rsquo; is used.
 </p></dd></dl>
 
+
 <p>See section <a href="/doc/master/userman/Coq-Proof-General#Quick-and-inconsistent-compilation">Quick and inconsistent compilation</a> for enabling vos compilation
 inside Proof General and see See section <a href="/doc/master/userman/Coq-Proof-General#Omitting-proofs-for-speed">Omitting proofs for speed</a> for the
 omit-proofs feature.
 </p>
-<p>The interactive use of this commands is limited because it only works
-on the current buffer. However, this commands can also be run in batch
-mode in a script, for instance in a continuous integration
-environment. To run this command on a file in batch mode, use
+<p>The interactive use of <code>proof-check-report</code> and
+<code>proof-check-annotate</code> is limited because they only work on the
+current buffer. However, these commands can also be run in batch mode
+in a script, for instance in a continuous integration environment. To
+run <code>proof-check-report</code> on a file in batch mode, use
 </p>
 <pre class="verbatim">emacs -batch -l &lt;your-pg-dir&gt;/generic/proof-site.el &lt;file&gt; \
-      --eval '(proof-check-proofs &lt;tap&gt; &lt;output&gt;)'
+      --eval '(proof-check-report &lt;tap&gt; &lt;output&gt;)'
 </pre>
 <p>where <code>&lt;tap&gt;</code> should be <code>nil</code> for human readable output and
 <code>t</code> for test anything protocol. If <code>&lt;output&gt;</code> is <code>t</code>
 the proof status appears in the standard output of the Emacs process.
 Otherwise <code>&lt;output&gt;</code> should be a filename as string in double
-quotes. Then the proof status is appended to this file. (If
+quotes. Then the proof status is written to this file. (If
 <code>output</code> is <code>nil</code> or omitted, the proof status is only put
 into the <code>*proof-check-report*</code> buffer, which does not make much
 sense in a batch command as the one above.)
 </p>
+<p>Using a similar command also <code>proof-check-annotate</code> can run in
+batch mode in a continuous integration environment, for instance for
+checking that all failing proofs are annotated with <code>FAIL</code>
+via <code>git diff --exit-code</code>.
+</p>
 
 <hr size="6">
 <a class="anchor" id="Automatic-multiple-file-handling"></a>
@@ -627,7 +688,7 @@ <h2 class="section">3.11 Editing features</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Basic-Script-Management.html b/doc/master/userman/Basic-Script-Management.html
index 9f90a39..7df944d 100644
--- a/doc/master/userman/Basic-Script-Management.html
+++ b/doc/master/userman/Basic-Script-Management.html
@@ -1109,7 +1109,7 @@ <h2 class="section">2.9 Interrupting during trace output</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Bugs-and-Enhancements.html b/doc/master/userman/Bugs-and-Enhancements.html
index d3ccde6..0232699 100644
--- a/doc/master/userman/Bugs-and-Enhancements.html
+++ b/doc/master/userman/Bugs-and-Enhancements.html
@@ -50,7 +50,7 @@ <h1 class="appendix">B. Bugs and Enhancements</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Concept-Index.html b/doc/master/userman/Concept-Index.html
index 39b1762..fe07505 100644
--- a/doc/master/userman/Concept-Index.html
+++ b/doc/master/userman/Concept-Index.html
@@ -180,8 +180,8 @@ <h1 class="unnumbered">Concept Index</h1>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Basic-Script-Management#index-proof-script-mode">proof script mode</a></td><td valign="top"><a href="/doc/master/userman/Basic-Script-Management#Script-buffers">2.3 Script buffers</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#index-Proof-status-statistic">Proof status statistic</a></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Proof-status-statistic">3.8 Proof status statistic</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Coq-Proof-General#index-Proof-using">Proof using</a></td><td valign="top"><a href="/doc/master/userman/Coq-Proof-General#Proof-using-annotations">10.3 Proof using annotations</a></td></tr>
-<tr><td></td><td valign="top"><a href="/doc/master/userman/Graphical-Proof_002dTree-Visualization#index-proof_002dtree-visualization">proof-tree visualization</a></td><td valign="top"><a href="/doc/master/userman/Graphical-Proof_002dTree-Visualization#Graphical-Proof_002dTree-Visualization">7. Graphical Proof-Tree Visualization</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Coq-Proof-General#index-Proof_002dTree-visualization">Proof-Tree visualization</a></td><td valign="top"><a href="/doc/master/userman/Coq-Proof-General#Proof_002dTree-Visualization">10.11 Proof-Tree Visualization</a></td></tr>
+<tr><td></td><td valign="top"><a href="/doc/master/userman/Graphical-Proof_002dTree-Visualization#index-proof_002dtree-visualization">proof-tree visualization</a></td><td valign="top"><a href="/doc/master/userman/Graphical-Proof_002dTree-Visualization#Graphical-Proof_002dTree-Visualization">7. Graphical Proof-Tree Visualization</a></td></tr>
 <tr><td colspan="3"> <hr></td></tr>
 <tr><th><a class="anchor" id="Concept-Index-1_cp_letter-Q">Q</a></th><td></td><td></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#index-Query-program-name">Query program name</a></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#User-options">8.4 User options</a></td></tr>
@@ -286,7 +286,7 @@ <h1 class="unnumbered">Concept Index</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Coq-Proof-General.html b/doc/master/userman/Coq-Proof-General.html
index 7de0737..67dba76 100644
--- a/doc/master/userman/Coq-Proof-General.html
+++ b/doc/master/userman/Coq-Proof-General.html
@@ -1028,7 +1028,7 @@ <h2 class="section">10.5 Omitting proofs for speed</h2>
 <a class="anchor" id="Proof-status-statistic-for-Coq-1"></a>
 <h2 class="section">10.6 Proof status statistic for Coq</h2>
 
-<p>The command <code>proof-check-proofs</code> (menu <code>Proof-General -&gt;
+<p>The command <code>proof-check-report</code> (menu <code>Proof-General -&gt;
 Check Opaque Proofs</code>) generates the proof status of all opaque proofs
 in the current buffer, i.e., it generates an overview that shows which
 of the opaque proofs in the current buffer are currently valid and
@@ -1036,7 +1036,14 @@ <h2 class="section">10.6 Proof status statistic for Coq</h2>
 where invalid proofs are permitted and vos compilation (See section <a href="#Quick-and-inconsistent-compilation">Quick and inconsistent compilation</a>) and the omit proofs feature
 (See section <a href="#Omitting-proofs-for-speed">Omitting proofs for speed</a>) are used to work at the most
 interesting or challenging point instead of on the first invalid
-proof. See See section <a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Proof-status-statistic">Proof status statistic</a> for more details.
+proof.
+</p>
+<p>The command <code>proof-check-annotate</code> (menu <code>Proof-General -&gt;
+Annotate Failing Proofs</code>) can then be used to consistently annotate
+failing proofs with a <code>FAIL</code> comment or to check, e.g., in
+continuous integration, that such comments are present.
+</p>
+<p>See See section <a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Proof-status-statistic">Proof status statistic</a> for more details.
 </p>
 
 <hr size="6">
@@ -1330,7 +1337,7 @@ <h2 class="section">10.13 Opam-switch-mode support</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Customizing-Proof-General.html b/doc/master/userman/Customizing-Proof-General.html
index d51ff83..1676e2a 100644
--- a/doc/master/userman/Customizing-Proof-General.html
+++ b/doc/master/userman/Customizing-Proof-General.html
@@ -778,7 +778,7 @@ <h2 class="section">8.6 Tweaking configuration settings</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/EasyCrypt-Proof-General.html b/doc/master/userman/EasyCrypt-Proof-General.html
index 3b26162..fd390cb 100644
--- a/doc/master/userman/EasyCrypt-Proof-General.html
+++ b/doc/master/userman/EasyCrypt-Proof-General.html
@@ -101,7 +101,7 @@ <h2 class="section">11.3 EasyCrypt customizations</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Function-Index.html b/doc/master/userman/Function-Index.html
index 213ba0b..b0640f9 100644
--- a/doc/master/userman/Function-Index.html
+++ b/doc/master/userman/Function-Index.html
@@ -59,7 +59,8 @@ <h1 class="unnumbered">Function and Command Index</h1>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Basic-Script-Management#index-proof_002dassert_002duntil_002dpoint_002dinteractive"><code>proof-assert-until-point-interactive</code></a></td><td valign="top"><a href="/doc/master/userman/Basic-Script-Management#Script-processing-commands">2.6 Script processing commands</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#index-proof_002dautosend_002dtoggle"><code>proof-autosend-toggle</code></a></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Automatic-processing">3.2 Automatic processing</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#index-proof_002dboring_002dface"><code>proof-boring-face</code></a></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#Goals-and-response-faces">8.5.2 Goals and response faces</a></td></tr>
-<tr><td></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#index-proof_002dcheck_002dproofs"><code>proof-check-proofs</code></a></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Proof-status-statistic">3.8 Proof status statistic</a></td></tr>
+<tr><td></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#index-proof_002dcheck_002dannotate"><code>proof-check-annotate</code></a></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Proof-status-statistic">3.8 Proof status statistic</a></td></tr>
+<tr><td></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#index-proof_002dcheck_002dreport"><code>proof-check-report</code></a></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Proof-status-statistic">3.8 Proof status statistic</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Basic-Script-Management#index-proof_002dctxt"><code>proof-ctxt</code></a></td><td valign="top"><a href="/doc/master/userman/Basic-Script-Management#Proof-assistant-commands">2.7 Proof assistant commands</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#index-proof_002ddebug_002dmessage_002dface"><code>proof-debug-message-face</code></a></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#Goals-and-response-faces">8.5.2 Goals and response faces</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#index-proof_002ddeclaration_002dname_002dface"><code>proof-declaration-name-face</code></a></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#Script-buffer-faces">8.5.1 Script buffer faces</a></td></tr>
@@ -139,7 +140,7 @@ <h1 class="unnumbered">Function and Command Index</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Graphical-Proof_002dTree-Visualization.html b/doc/master/userman/Graphical-Proof_002dTree-Visualization.html
index f443ebc..e2ff0b7 100644
--- a/doc/master/userman/Graphical-Proof_002dTree-Visualization.html
+++ b/doc/master/userman/Graphical-Proof_002dTree-Visualization.html
@@ -152,7 +152,7 @@ <h2 class="section">7.3 Prooftree Customization</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Hints-and-Tips.html b/doc/master/userman/Hints-and-Tips.html
index 742f47f..e7d395b 100644
--- a/doc/master/userman/Hints-and-Tips.html
+++ b/doc/master/userman/Hints-and-Tips.html
@@ -211,7 +211,7 @@ <h2 class="section">9.3 Using abbreviations</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/History-of-Proof-General.html b/doc/master/userman/History-of-Proof-General.html
index 568e84a..1d639a5 100644
--- a/doc/master/userman/History-of-Proof-General.html
+++ b/doc/master/userman/History-of-Proof-General.html
@@ -379,7 +379,7 @@ <h2 class="unnumberedsec">Old News for 3.7</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Introducing-Proof-General.html b/doc/master/userman/Introducing-Proof-General.html
index 925baee..84bd340 100644
--- a/doc/master/userman/Introducing-Proof-General.html
+++ b/doc/master/userman/Introducing-Proof-General.html
@@ -351,7 +351,7 @@ <h2 class="section">1.6 Organization of this manual</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Keystroke-Index.html b/doc/master/userman/Keystroke-Index.html
index 701161f..6720dee 100644
--- a/doc/master/userman/Keystroke-Index.html
+++ b/doc/master/userman/Keystroke-Index.html
@@ -77,7 +77,7 @@ <h1 class="unnumbered">Keystroke Index</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Obtaining-and-Installing.html b/doc/master/userman/Obtaining-and-Installing.html
index d9f09f3..539e1e2 100644
--- a/doc/master/userman/Obtaining-and-Installing.html
+++ b/doc/master/userman/Obtaining-and-Installing.html
@@ -187,7 +187,7 @@ <h3 class="unnumberedsubsec">Removing support for unwanted provers</h3>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Preface.html b/doc/master/userman/Preface.html
index 0baf73c..e68d48e 100644
--- a/doc/master/userman/Preface.html
+++ b/doc/master/userman/Preface.html
@@ -322,7 +322,7 @@ <h2 class="unnumberedsec">Credits</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/ProofGeneral_22.html b/doc/master/userman/ProofGeneral_22.html
index e2d4ffa..ca50b36 100644
--- a/doc/master/userman/ProofGeneral_22.html
+++ b/doc/master/userman/ProofGeneral_22.html
@@ -154,7 +154,7 @@ <h1 class="unnumbered">Concept Index: U &ndash; X</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/ProofGeneral_abt.html b/doc/master/userman/ProofGeneral_abt.html
index e9a4eae..ea0dc41 100644
--- a/doc/master/userman/ProofGeneral_abt.html
+++ b/doc/master/userman/ProofGeneral_abt.html
@@ -14,7 +14,7 @@
 </div>
 <h1>About This Document</h1>
 <p>
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
 </p>
 <p>
   The buttons in the navigation panels have the following meaning:
@@ -124,7 +124,7 @@ <h1>About This Document</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/ProofGeneral_fot.html b/doc/master/userman/ProofGeneral_fot.html
index 7535eda..478313d 100644
--- a/doc/master/userman/ProofGeneral_fot.html
+++ b/doc/master/userman/ProofGeneral_fot.html
@@ -51,7 +51,7 @@ <h3><a id="FOOT1" href="/doc/master/userman/Introducing-Proof-General#DOCF1">(1)
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/ProofGeneral_toc.html b/doc/master/userman/ProofGeneral_toc.html
index c058861..fb1680a 100644
--- a/doc/master/userman/ProofGeneral_toc.html
+++ b/doc/master/userman/ProofGeneral_toc.html
@@ -192,7 +192,7 @@ <h1>Table of Contents</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/References.html b/doc/master/userman/References.html
index 4c8e3f4..1606ba7 100644
--- a/doc/master/userman/References.html
+++ b/doc/master/userman/References.html
@@ -64,7 +64,7 @@ <h1 class="unnumbered">References</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Shell-Proof-General.html b/doc/master/userman/Shell-Proof-General.html
index 4dee2ee..af260e2 100644
--- a/doc/master/userman/Shell-Proof-General.html
+++ b/doc/master/userman/Shell-Proof-General.html
@@ -60,7 +60,7 @@ <h1 class="chapter">12. Shell Proof General</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Subterm-Activation-and-Proof-by-Pointing.html b/doc/master/userman/Subterm-Activation-and-Proof-by-Pointing.html
index 7bb7382..5c979bf 100644
--- a/doc/master/userman/Subterm-Activation-and-Proof-by-Pointing.html
+++ b/doc/master/userman/Subterm-Activation-and-Proof-by-Pointing.html
@@ -124,7 +124,7 @@ <h2 class="section">6.1 Goals buffer commands</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Support-for-other-Packages.html b/doc/master/userman/Support-for-other-Packages.html
index e8947ce..8194b55 100644
--- a/doc/master/userman/Support-for-other-Packages.html
+++ b/doc/master/userman/Support-for-other-Packages.html
@@ -271,7 +271,7 @@ <h2 class="section">5.5 Support for tags</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Unicode-symbols-and-special-layout-support.html b/doc/master/userman/Unicode-symbols-and-special-layout-support.html
index 6e74e3a..e7f5021 100644
--- a/doc/master/userman/Unicode-symbols-and-special-layout-support.html
+++ b/doc/master/userman/Unicode-symbols-and-special-layout-support.html
@@ -454,7 +454,7 @@ <h2 class="section">4.7 Selecting suitable fonts</h2>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/Variable-Index.html b/doc/master/userman/Variable-Index.html
index 2ad4bcc..f3e7f42 100644
--- a/doc/master/userman/Variable-Index.html
+++ b/doc/master/userman/Variable-Index.html
@@ -67,6 +67,8 @@ <h1 class="unnumbered">Variable and User Option Index</h1>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#index-proof_002dauto_002daction_002dwhen_002ddeactivating_002dscripting"><code>proof-auto-action-when-deactivating-scripting</code></a></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#User-options">8.4 User options</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#index-proof_002dauto_002draise_002dbuffers"><code>proof-auto-raise-buffers</code></a></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#Display-customization">8.3 Display customization</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#index-proof_002dautosend_002denable"><code>proof-autosend-enable</code></a></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Automatic-processing">3.2 Automatic processing</a></td></tr>
+<tr><td></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#index-proof_002dcheck_002dannotate_002dposition"><code>proof-check-annotate-position</code></a></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Proof-status-statistic">3.8 Proof status statistic</a></td></tr>
+<tr><td></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#index-proof_002dcheck_002dannotate_002dright_002dmargin"><code>proof-check-annotate-right-margin</code></a></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Proof-status-statistic">3.8 Proof status statistic</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#index-proof_002dcolour_002dlocked"><code>proof-colour-locked</code></a></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#Display-customization">8.3 Display customization</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#index-proof_002ddelete_002dempty_002dwindows"><code>proof-delete-empty-windows</code></a></td><td valign="top"><a href="/doc/master/userman/Customizing-Proof-General#Display-customization">8.3 Display customization</a></td></tr>
 <tr><td></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#index-proof_002ddisappearing_002dproofs"><code>proof-disappearing-proofs</code></a></td><td valign="top"><a href="/doc/master/userman/Advanced-Script-Management-and-Editing#Visibility-of-completed-proofs">3.3 Visibility of completed proofs</a></td></tr>
@@ -123,7 +125,7 @@ <h1 class="unnumbered">Variable and User Option Index</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>
 
diff --git a/doc/master/userman/index.html b/doc/master/userman/index.html
index 5375539..d5bf1d3 100644
--- a/doc/master/userman/index.html
+++ b/doc/master/userman/index.html
@@ -78,7 +78,7 @@ <h1 class="settitle">Proof General</h1>
 </div>
 <p>
  <font size="-1">
-  This document was generated on <i>May 2, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
+  This document was generated on <i>May 13, 2024</i> using <a href="http://www.nongnu.org/texi2html/"><i>texi2html 1.82</i></a>.
  </font>
  <br>