diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2001-08-28 15:53:17 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2001-08-28 15:53:17 +0000 |
| commit | 2bf4a7f0b3cf660c6b215a3e49d80115409e192e (patch) | |
| tree | 44aa3864c49b9815d7a485a8120609168a7740b2 /lego | |
| parent | eef850dfb660ad59a4d25fce00dc322942a44a83 (diff) | |
Change of proof span type back to goalsave
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego.el | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lego/lego.el b/lego/lego.el index 087b775a..ea49805f 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -207,7 +207,7 @@ Given is the first SPAN which needs to be undone." ((eq (span-property span 'type) 'comment)) - ((eq (span-property span 'type) 'proof) + ((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))))) ;; alternative definitions |