[nongnu] elpa/proof-general eb468a9f8f 08/11: user doc, CHANGES: update for prooftree

[ELPA Syncer]

branch: elpa/proof-general
commit eb468a9f8f0b537afffbff4bee33d4479091e91d
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>

    user doc, CHANGES: update for prooftree
---
 CHANGES               | 11 +++++++++--
 doc/ProofGeneral.texi | 14 ++++++++------
 2 files changed, 17 insertions(+), 8 deletions(-)

diff --git a/CHANGES b/CHANGES
index b84ed46067..1e29c5542e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,15 +8,22 @@ the Git ChangeLog, the GitHub repo 
https://github.com/ProofGeneral/PG
 ** Generic changes
 *** Improve the omit-proofs feature to handle a number of cases where
     proofs must not be omitted.
+*** Renew support for proof-tree visualization via the external command
+    prooftree, see http://askra.de/software/prooftree and Section 7
+    "Graphical Proof-Tree Visualization" in the Proof General manual.
+    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.
 
 ** Coq changes
-
 *** support Coq 8.19
-
 **** New option coq-compile-coqdep-warnings to configure the warning
      command line argument (-w) of coqdep. The default of this option
      is +module-not-found to let Proof General reliably detect missing
      modules as coqdep error.
+*** Renew support for proof-tree visualization, see description in
+    generic changes above.
+
 
 **** Fix issues #687 and #688 where the omit-proofs feature causes
      errors on correct code.
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 6ddf7638ae..c0158d63c1 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3172,12 +3172,14 @@ Query the prover about the identifier near mouse click 
@var{event}.
 @chapter Graphical Proof-Tree Visualization
 @cindex proof-tree visualization
 
-Since version 4.2, Proof General supports proof-tree
+Since version 4.5, Proof General (again) supports proof-tree
 visualization on graphical desktops via the additional program
-Prooftree. Currently, proof-tree visualization is only supported
-for the Coq proof assistant. 
+Prooftree. Currently, proof-tree visualization is only supported for
+the Coq proof assistant. (Proof-tree visualization was already
+supported in version 4.2 but then discontinued in 2017 when Coq 8.7
+dropped the variant of @code{Show Goal} that prooftree relied on.)
 
-This version of Proof General requires Prooftree version 0.11.
+This version of Proof General requires Prooftree version 0.14.
 Check the @uref{http://askra.de/software/prooftree/, Prooftree website},
 to see if some later versions are also compatible. (Because of
 the communication protocol, Proof General is always only
@@ -5349,8 +5351,8 @@ you want to save abbrevs; answer yes.
 @section Proof-Tree Visualization
 @cindex Proof-Tree visualization
 
-Starting with Proof General version 4.2 and Coq version 8.4, Coq
-Proof General has full support for proof-tree visualization, 
+Starting with Proof General version 4.5 and Coq version 8.11, Coq
+Proof General has (again) full support for proof-tree visualization, 
 @pxref{Graphical Proof-Tree Visualization}. To find out which
 versions of Prooftree are compatible with this version of Proof
 General, @pxref{Graphical Proof-Tree Visualization} or the