documented problem with Discharge in LEGO

1 files changed, 6 insertions, 0 deletions

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.