diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 13 |
2 files changed, 9 insertions, 6 deletions
@@ -21,7 +21,7 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. to compile modules in parallel in the background while Proof General stays responsive. -*** Support for bullets and braces for Prooftree. +*** Support for bullets, braces and Grab Existential Variables for Prooftree. * Changes of Proof General 4.2 from Proof General 4.1 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 |