Updated.

2 files changed, 4 insertions, 9 deletions

diff --git a/CHANGES b/CHANGES
index 0f980d1a..12356d4f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,7 +15,10 @@
 
 ** Generic changes
 
+*** Display management: added shring-windows-tofit option
 
+Attempt to shrink output windows to fit their contents in
+case it is less than 1/2 the window height.  In progress.  
 
 *** Parsing internals changed: minor user visible differences
 
diff --git a/coq/BUGS b/coq/BUGS
index d4df41c3..42cc2a28 100644
--- a/coq/BUGS
+++ b/coq/BUGS
@@ -4,10 +4,6 @@
 
 See also ../BUGS for generic bugs.
 
-** X-Symbol does not work on GNU Emacs.  
-
-Please don't even try it, it will mess up your Emacs.  
-
 ** With new syntax in Coq 7, comments at end of files cannot be processed.
 
 Leads to annoying retract/process questions when switching buffers.
@@ -19,11 +15,7 @@ It cannot handle lists e.g., with "Parameter x,y:nat" it only tags x
 but not y. [The same problem exists for legotags] Workaround: don't
 rely too much on the etags mechanism.
 
-** User defined tactics cannot be retracted. 
-
- Workaround: you may need to retract to the beginning of the proof.
-
-** Coq Proof General does not know about Coq's Section mechanism.
+** With Coq 7, multiple file handling and auto-compilation is buggy
 
 ** Surely others that aren't mentioned here...