From f916f8a84abd57b8cdd3ef7bc54c96b88c268076 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 13 Dec 2007 12:59:09 +0000
Subject: Updated.

---
 coq/BUGS | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

(limited to 'coq')

diff --git a/coq/BUGS b/coq/BUGS
index 8dfe90f9..6599180a 100644
--- a/coq/BUGS
+++ b/coq/BUGS
@@ -4,21 +4,17 @@
 
 See also ../BUGS for generic bugs.
 
-** With new syntax in Coq 7, comments at end of files cannot be processed.
+** Multiple file handling and auto-compilation is incomplete
 
-Leads to annoying retract/process questions when switching buffers.
-Workaround: don't use a comment as the last line of the buffer, for now.
+** C-c C-a C-i on long intro lines breaks line the wrong way.
 
 ** coqtags doesn't find all declarations. 
 
 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.
-
-** With Coq 7, multiple file handling and auto-compilation is buggy
-
-** Surely others that aren't mentioned here...
   
-Please report them to da+pg-bugs@inf.ed.ac.uk
+** Others not mentioned...
+
+Please report further issues at http://proofgeneral.inf.ed.ac.uk/trac
 
-** C-c C-a C-i on long intro lines breaks line the wrong way.
\ No newline at end of file
-- 
cgit v1.2.3