From 7139ed1fbdcab00bb678e4a9897f3d80bd087098 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 13 Sep 2000 14:59:06 +0000
Subject: Remove ambitious promise to implement proper generic-find-and-forget.

---
 generic/proof-script.el | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'generic/proof-script.el')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index a3b7d63e..c3a22a4c 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2790,13 +2790,12 @@ This is a long-range forget: we know that there is no
 open goal at the moment, so forgetting involves unbinding
 declarations, etc, rather than undoing proof steps.
 
-CURRENTLY UNIMPLEMENTED: just returns proof-no-command.
-Check the lego-find-and-forget or coq-find-and-forget
-functions for examples of how to write this function.
+Currently this has a trivial implementation: it 
+just returns proof-no-command, meaning `do nothing'.
 
-In the next release of Proof General, there will be
-a generic implementation of this."
-  ;; FIXME: come true on the promise above!
+Check the lego-find-and-forget or coq-find-and-forget
+functions for examples of how to write this function."
+  ;; FIXME: implement a useful generic find-and-forget
   proof-no-command)
 
 ;;
-- 
cgit v1.2.3