aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--generic/pg-user.el2
-rw-r--r--isar/isar.el2
2 files changed, 2 insertions, 2 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 9aba625f..0666b7b9 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -114,7 +114,7 @@ the proof script."
(proof-maybe-save-point
(let
((span (proof-last-goal-or-goalsave)))
- (if (and span (not (eq (span-property span 'type) 'goalsave))
+ (if (and span (not (eq (span-property span 'type) 'proof))
(< (span-end span) (proof-unprocessed-begin)))
(progn
(goto-char (span-start span))
diff --git a/isar/isar.el b/isar/isar.el
index fb7f33f0..d9e7e7a2 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -367,7 +367,7 @@ proof-shell-retract-files-regexp."
((or (eq (span-property span 'type) 'comment)
(proof-string-match isar-undo-skip-regexp str)))
;; finished goal: undo
- ((eq (span-property span 'type) 'goalsave)
+ ((eq (span-property span 'type) 'proof)
(setq ans isar-undo))
;; open goal: skip and exit
((proof-string-match isar-goal-command-regexp str)