From 176c2ea7966af858cd501b88762fbed378f00698 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 15 Apr 2004 13:31:36 +0000
Subject: Updated.

---
 BUGS         | 6 ++++++
 CHANGES      | 2 +-
 etc/announce | 2 +-
 todo         | 8 ++++++++
 4 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/BUGS b/BUGS
index 505533e8..3008e61a 100644
--- a/BUGS
+++ b/BUGS
@@ -15,6 +15,12 @@ versions, and those which only apply to particular versions.
 
 * Generic problems, for all Emacs versions
 
+** X-Symbol support removed from "secondary" provers (HOL, ACL2, LEGO, Twelf)
+
+If anyone was actually using this, please let me know.  It should be
+very easy to revive by copying coq/x-symbol-coq.el (although a generic
+version might be desirable).
+
 ** Visibility control doesn't distinguish theorems with same name.
 
 If you have more than one theorem with the same name in a buffer,
diff --git a/CHANGES b/CHANGES
index a48209f5..84f77586 100644
--- a/CHANGES
+++ b/CHANGES
@@ -204,7 +204,7 @@ APIs), then you may have to upgrade your Isabelle version as well.
 
 ** Changes for Coq
 
-*** Indentation
+*** Indentation improved
 
 *** Menu entries for commands, tactics and terms
 
diff --git a/etc/announce b/etc/announce
index a8d1aa31..5a28a99b 100644
--- a/etc/announce
+++ b/etc/announce
@@ -7,7 +7,7 @@
 Proof General is a generic (X)Emacs interface for proof assistants.
 It can be instantiated for the proof assistant of your choice, and is
 supplied ready-customised for Isabelle, Coq, LEGO, and PhoX, and, 
-experimentally, for HOL98, Twelf, and ACL2.
+experimentally, several other systems.
 
 Proof General includes these features, amongst others:
 
diff --git a/todo b/todo
index 7367c3e2..26de88cf 100644
--- a/todo
+++ b/todo
@@ -95,6 +95,14 @@ X (Low)		e.g. probably not worth spending time on
 *** PGIP SUPPORT (minimal for Isabelle patch):
       -- settings with categories
 
+*** A Oddity: Weirdness with regions turning blue even though they
+    haven't been processed.  Noticed with HOL/CCC experimental setups.
+    Send a few regions queueing, no result from interpreter, yet sometimes
+    turns blue.  Why???
+
+*** Allow empty retract action that doesn't produce new prompt
+    (Noticed with HOL4).
+
 *** [ Don't query save before retraction ?? ]
 
 *** C Implement optional arg to next/undo which doesn't update
-- 
cgit v1.2.3