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 | |
| parent | eef850dfb660ad59a4d25fce00dc322942a44a83 (diff) | |
Change of proof span type back to goalsave
| -rw-r--r-- | coq/coq.el | 2 | ||||
| -rw-r--r-- | isar/isar.el | 2 | ||||
| -rw-r--r-- | lego/lego.el | 2 | ||||
| -rw-r--r-- | phox/phox-fun.el | 2 |
4 files changed, 4 insertions, 4 deletions
@@ -203,7 +203,7 @@ ((eq (span-property span 'type) 'comment)) - ((eq (span-property span 'type) 'proof) + ((eq (span-property span 'type) 'goalsave) ;; Note da 6.10.99: in Lego and Isabelle, it's trivial to ;; forget an unnamed theorem. Coq really does use the ;; identifier "Unnamed_thm", though! So we don't need diff --git a/isar/isar.el b/isar/isar.el index d1a27bec..ba8d4469 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -371,7 +371,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) 'proof) + ((eq (span-property span 'type) 'goalsave) (setq ans isar-undo)) ;; open goal: skip and exit ((proof-string-match isar-goal-command-regexp str) 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 diff --git a/phox/phox-fun.el b/phox/phox-fun.el index 22d3e717..7592a87e 100644 --- a/phox/phox-fun.el +++ b/phox/phox-fun.el @@ -173,7 +173,7 @@ or for optional argument TABLE." ((eq (span-property span 'type) 'comment)) - ((eq (span-property span 'type) 'proof) + ((eq (span-property span 'type) 'goalsave) (if (proof-string-match phox-prove-claim-regexp str) (setq ans (concat (format phox-forget-proof-command (match-string 4 str)) ans)) |