From c8a997a20215220f2f79ffc1cb34de758e73538c Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Thu, 17 Jan 2013 09:09:29 +0000 Subject: document latest changes --- doc/ProofGeneral.texi | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'doc') diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 58119672..628fae0f 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4893,12 +4893,15 @@ versions of Prooftree are compatible with this version of Proof General, @pxref{Graphical Proof-Tree Visualization} or the @uref{http://askra.de/software/prooftree/, Prooftree website}. -Proof-tree visualization does currently not support the command -``Grab Existential Variables''. - For the visualization to work properly, proofs must be started -with ``Proof.'', which is encouraged practice anyway (see Coq Bug -#2776). +with @code{Proof}, which is encouraged practice anyway (see Coq Bug +#2776). Without @code{Proof} you lose the initial proof goal, +possibly having two or more initial goals in the display. + +To support @code{Grab Existential Variables} Prooftree can +actually display several graphically independent proof trees in +several layers. + @c ================================================================= @c -- cgit v1.2.3