From 4ae205b8cd8dd8f0b5f8ac8308e63246733e70fd Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 9 Sep 2001 16:57:55 +0000
Subject: Bug in new parsing for coq, mention

---
 coq/BUGS | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/coq/BUGS b/coq/BUGS
index 11d43ef8..daf31a4d 100644
--- a/coq/BUGS
+++ b/coq/BUGS
@@ -4,6 +4,12 @@
 
 See also ../BUGS for generic bugs.
 
+** With new syntax in Coq 7, comments at end of files cannot be processed.
+
+Leads to annoying retract/process questions when switching buffers.
+Workaround: don't use a comment as the last line of the buffer, for now.
+
+
 ** coqtags doesn't find all declarations. 
 
 It cannot handle lists e.g., with "Parameter x,y:nat" it only tags x
-- 
cgit v1.2.3