From ffdefe0319d76aa039ab91f193ed2e244f6bc509 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Tue, 10 Nov 1998 15:25:38 +0000
Subject: documented problem with Discharge in LEGO

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

(limited to 'BUGS')

diff --git a/BUGS b/BUGS
index 8bfb6856..be0f5e1b 100644
--- a/BUGS
+++ b/BUGS
@@ -59,6 +59,12 @@ FSF Emacs specific bugs
 LEGO Proof General Bugs
 =======================
 
+* After a `Discharge', retraction ought to only be possible back to the
+first declaration/definition which is discharged. However, LEGO Proof
+General does not know that Discharge has such a non-local effect.
+Workaround: retract back to the first declaration/definition which is
+discharged.
+
 * A thorny issues are local definitions in a proof state. LEGO cannot
 undo them explicitly. Workaround: retract back to a command before a
 definition.
-- 
cgit v1.2.3