diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2013-01-17 09:09:29 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2013-01-17 09:09:29 +0000 |
| commit | c8a997a20215220f2f79ffc1cb34de758e73538c (patch) | |
| tree | 3a9b45d28e8f049955ee6f5cb6342d0846078d46 /doc | |
| parent | 88343f978a0e09f1673ccec228fc7ab9c98d46e7 (diff) | |
document latest changes
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 13 |
1 files changed, 8 insertions, 5 deletions
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 |