aboutsummaryrefslogtreecommitdiffhomepage
path: root/lego
diff options
context:
space:
mode:
Diffstat (limited to 'lego')
-rw-r--r--lego/lego.el2
1 files changed, 2 insertions, 0 deletions
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)))))