From d5408248f4f8ce638d313fc656b7ed3a4069129a Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Mon, 21 Jan 2013 14:13:56 +0000 Subject: - implement proof-script insertion --- CHANGES | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 4dec4118..e2969690 100644 --- a/CHANGES +++ b/CHANGES @@ -6,12 +6,19 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. * Changes of Proof General 4.3 from Proof General 4.2 -** Generic/misc changes +** Prooftree changes *** Require Prooftree version 0.11 Check the Prooftree website to see which other versions of Prooftree are compatible with Proof General 4.3. +*** New features + One can now trigger an retraction (undo) by selecting the + appropriate sequent in Prooftree. One can further send proof + commands or proof scripts from whole proof subtrees to Proof + General, which will insert them in the current buffer. + Prooftree also supports some recent Coq features, see below. + ** Coq changes *** Asynchronous parallel compilation of required modules @@ -23,6 +30,7 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. *** Support for bullets, braces and Grab Existential Variables for Prooftree. + * Changes of Proof General 4.2 from Proof General 4.1 ** Generic/misc changes -- cgit v1.2.3