aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
authorHendrik Tews2012-01-03 10:40:39 +0000
committerHendrik Tews2012-01-03 10:40:39 +0000
commit9e106ef2d8377a8a12285eb79e5a704751cebdcb (patch)
tree3c902df85104600b7cc600e44c548ba94db0f6bb /CHANGES
parent413d5721b1dfb5f4d43c8e1676cd5def02f63423 (diff)
update CHANGES
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES8
1 files changed, 8 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index c3c3ce50..f4278cab 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,12 +8,20 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
** Generic/misc changes
+*** Support proof-tree visualization via the external Prooftree program
+ Currently only Coq (using Coq version 8.4beta or newer)
+ supports proof-tree visualization. If Prooftree is installed,
+ the proof-tree display can be started via the toolbar, the
+ Proof-General menu or by C-c C-d.
+
*** Compilation fixes for Emacs 24.
*** Fix "pgshell" mode for shell/CLI prover interaction
** Coq changes
+*** Support proof-tree visulization
+
*** Indentation improvements using SMIE
*** Minor parsing fixes