From 9c77766565cc9c29289ecf1c7d6c964d6af388ce Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 5 Jun 2003 10:45:12 +0000 Subject: Make find-and-forget robust for proverproc regions --- lego/lego.el | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lego') diff --git a/lego/lego.el b/lego/lego.el index 00a32319..d5b882b9 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -208,6 +208,8 @@ Given is the first SPAN which needs to be undone." ((eq (span-property span 'type) 'comment)) + ((eq (span-property span 'type) 'proverproc)) + ((eq (span-property span 'type) 'goalsave) (unless (eq (span-property span 'name) proof-unnamed-theorem-name) (setq ans (format lego-forget-id-command (span-property span 'name))))) -- cgit v1.2.3