user doc, CHANGES: update for prooftree

CHANGES

@@ -5,7 +5,18 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
 
 * Changes of Proof General 4.6 from Proof General 4.5
 
-N/A
+** Generic changes
+*** 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
+*** Renew support for proof-tree visualization, see description in
+    generic changes above.
+
 
 * Changes of Proof General 4.5 from Proof General 4.4
 

doc/ProofGeneral.texi

@@ -3157,12 +3157,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
@@ -5302,8 +5304,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