aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2002-07-18 23:27:09 +0000
committerDavid Aspinall2002-07-18 23:27:09 +0000
commita1e8f2592c8e889726047217e5ea36b68b17f93b (patch)
treeb13b51f706583d5f384026378d585852744cc87a
parent8716ccdb197c93a7ed13742b11ea72be01c3a646 (diff)
X-sym bug
-rw-r--r--coq/BUGS5
1 files changed, 4 insertions, 1 deletions
diff --git a/coq/BUGS b/coq/BUGS
index daf31a4d..d4df41c3 100644
--- a/coq/BUGS
+++ b/coq/BUGS
@@ -4,12 +4,15 @@
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.
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