Note recent changes

1 files changed, 15 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index 270bb1d4..d1de035f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,8 @@
 -*- outline -*-  
 
+This is a summary of main changes.  For details, please see
+the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
+
 * Changes of Proof General 4.1 from Proof General 4.0
 
 ** Generic changes
@@ -14,15 +17,22 @@
 ** Coq changes
 
 *** A new indentation algorithm, using SMIE.
-This is used by default if SMIE is available (Emacs >= 23.3), but is
-controlled by the variable `coq-use-smie'.  It also provides improved
-navigation facilities for things like C-M-t, C-M-f and C-M-b.
+    This is used by default if SMIE is available (Emacs >= 23.3), but is
+    controlled by the variable `coq-use-smie'.  It also provides improved
+    navigation facilities for things like C-M-t, C-M-f and C-M-b.
+    Addition by Stefan Monnier.
+
+*** Experimental multiple file handling for Coq.
+    Proof General is now able to automatically compile files while
+    scripting Require commands, either internally or externally (by
+    running Make).  Additionally, it will automatically retract 
+    buffers when switching to new files, to model separate compilation
+    properly.  For more details, see XXXX.
+    Addition by Hendrik Tews.
 
 *** Fixes for Coq 8.3
 
 
-
-
 * Main Changes for Proof General 4.0 from 3.7.1
 
 ** Install/support changes