From abbe9a4c9efd00952f2376eb79630f16f09e5b21 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 13 Mar 2000 07:34:30 +0000
Subject: BUGS for Coq.

---
 coq/BUGS | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 coq/BUGS

diff --git a/coq/BUGS b/coq/BUGS
new file mode 100644
index 00000000..b42de11b
--- /dev/null
+++ b/coq/BUGS
@@ -0,0 +1,19 @@
+-*- mode:outline -*-
+
+* Coq Proof General Bugs
+
+See also ../BUGS for generic bugs.
+
+** 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.
+
+** User defined tactics cannot be retracted. 
+
+ Workaround: you may need to retract to the beginning of the proof.
+
+** Surely others that aren't mentioned here...
+  
+  Please report them to proofgen@dcs.ed.ac.uk.
-- 
cgit v1.2.3