- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82. + This document was generated on May 13, 2024 using texi2html 1.82.
The buttons in the navigation panels have the following meaning: @@ -124,7 +124,7 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
The command proof-check-proofs 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 proof-check-proofs 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
-proof-script-proof-admit-command and the proof is considered
-invalid. To associate theorem names with opaque proofs, the function
-proof-get-proof-info-fn is called, which is identical to
-proof-tree-get-proof-info, See section Proof Tree Elisp configuration.
+
The commands proof-check-report and proof-check-annotate
+build on the omit-proofs feature. Using its machinery,
+proof-check-proofs, 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
+proof-check-proofs 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 proof-script-proof-admit-command and the proof is
+considered invalid. To associate theorem names with opaque proofs, the
+function proof-get-proof-info-fn is called, which is identical
+to proof-tree-get-proof-info, See section Proof Tree Elisp configuration.
To enable proof status statistics, the omit-proofs feature must be configured, See section Omitting proofs for speed. Additionally, the @@ -898,7 +899,7 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
The command The command proof-check-proofs (menu Proof-General ->
+proof-check-report (menu Proof-General ->
Check Opaque Proofs) 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 @@ 3.8 Proof status statistic
in the buffer *proof-check-report* (as long as
proof-check-report-buffer is not changed).
Currently proof-check-proofs does only work for Coq.
+
The command proof-check-annotate (menu Proof-General ->
+Annotate Failing Proofs) modifies the current buffer and places
+comments containing FAIL on all failing opaque proofs. With
+prefix argument also the passing proofs are annotated with
+PASS. For configuring the position of these comments, see
+proof-check-annotate-position and
+proof-check-annotate-right-margin.
+
Currently proof-check-report and proof-check-annotate
+only work for Coq.
Generate an overview about valid and invalid proofs.
This command completely processes the current buffer and
generates an overview about all the opaque proofs in it and
@@ -418,45 +427,97 @@
proof-check-report-buffer’. If batch is a string, it should be a
-filename and the overview is appended there. Otherwise the
-overview is output via ‘message’ 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 ‘message’ such that it appears on stdout when this
+command runs in batch mode.
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
'Defined' are not opaque and do not appear in the generated
overview.
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. +
Annotate failing proofs in current buffer with a "fail" comment.
+This function modifies the current buffer in place. Use with
+care!
+
Similarly to ‘proof-check-report’, check all opaque proofs in the
+current buffer. Instead of generating a report, failing proofs
+are annotated with "fail" in a comment. Existing "pass" or
+"fail" comments (e.g., from a previous run) are deleted
+together with the surrounding white space. With prefix argument
+(or when annotate-passing is non-nil) also passing proofs are
+annotated with a "pass" 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
+‘proof-check-annotate-position’ and
+‘proof-check-annotate-right-margin’.
+
Interactively, this command does not save the current buffer +after placing the annotations. With save-buffer non-nil, the +current buffer is saved if it has been modified. +
Line for annotating proofs with "pass" or "fail" comments.
+This option determines the line where ‘proof-check-annotate’ puts
+comments with "pass" and "fail". Value ‘’theoren’ 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 ‘’proof-using’ uses the first line of the
+last statement before the opaque proof, which corresponds to the
+Proof using line for Coq.
+
Right margin for "pass" and "fail" comments.
+This option determines the right margin to which
+‘proof-check-annotate’ right-aligns the comments with "pass"
+and "fail". If nil, the value of ‘fill-column’ is used.
See section Quick and inconsistent compilation for enabling vos compilation inside Proof General and see See section Omitting proofs for speed for the omit-proofs feature.
-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 +
The interactive use of proof-check-report and
+proof-check-annotate 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 proof-check-report on a file in batch mode, use
emacs -batch -l <your-pg-dir>/generic/proof-site.el <file> \ - --eval '(proof-check-proofs <tap> <output>)' + --eval '(proof-check-report <tap> <output>)'
where <tap> should be nil for human readable output and
t for test anything protocol. If <output> is t
the proof status appears in the standard output of the Emacs process.
Otherwise <output> 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
output is nil or omitted, the proof status is only put
into the *proof-check-report* buffer, which does not make much
sense in a batch command as the one above.)
Using a similar command also proof-check-annotate can run in
+batch mode in a continuous integration environment, for instance for
+checking that all failing proofs are annotated with FAIL
+via git diff --exit-code.
+
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
The command The command proof-check-proofs (menu Proof-General ->
+proof-check-report (menu Proof-General ->
Check Opaque Proofs) 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 @@ 10.6 Proof status statistic for Coq
where invalid proofs are permitted and vos compilation (See section Quick and inconsistent compilation) and the omit proofs feature
(See section Omitting proofs for speed) are used to work at the most
interesting or challenging point instead of on the first invalid
-proof. See See section Proof status statistic for more details.
+proof.
+
The command proof-check-annotate (menu Proof-General ->
+Annotate Failing Proofs) can then be used to consistently annotate
+failing proofs with a FAIL comment or to check, e.g., in
+continuous integration, that such comments are present.
+
See See section Proof status statistic for more details.
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
proof-assert-until-point-interactiveproof-autosend-toggleproof-boring-faceproof-check-proofsproof-check-annotateproof-check-reportproof-ctxtproof-debug-message-faceproof-declaration-name-face
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82. + This document was generated on May 13, 2024 using texi2html 1.82.
The buttons in the navigation panels have the following meaning: @@ -124,7 +124,7 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
proof-auto-action-when-deactivating-scriptingproof-auto-raise-buffersproof-autosend-enableproof-check-annotate-positionproof-check-annotate-right-marginproof-colour-lockedproof-delete-empty-windowsproof-disappearing-proofs
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.
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 @@
- This document was generated on May 2, 2024 using texi2html 1.82.
+ This document was generated on May 13, 2024 using texi2html 1.82.