diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-06-05 11:11:17 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-06-05 11:11:17 +0000 |
| commit | 98998e82ff24e927c77b9b110fd32aeac49b2a39 (patch) | |
| tree | 0c783d3858c3d7fa3a2506992a856ca8c1aabf5e /generic/proof-script.el | |
| parent | f0627f22629aa60c93cd18c906c0c61ac0cf25c9 (diff) | |
Typo
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index f7301ffc..ffad55be 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1252,7 +1252,8 @@ With ARG, turn on scripting iff ARG is positive." ;; extent as argument. Seems odd. (proof-debug "Proof General idiosyncrasy: proof-done-advancing called with a dead span!") - ;; + + ;; otherwise... (let ((end (span-end span)) (cmd (span-property span 'cmd))) ;; State of spans after advancing: @@ -1379,7 +1380,7 @@ With ARG, turn on scripting iff ARG is positive." (setq cmd (span-property gspan 'cmd)) (cond ;; Ignore comments [may have null cmd setting] - ((eq (span-property span 'type) 'comment)) + ((eq (span-property gspan 'type) 'comment)) ;; Nested goal saves: add in any nestedcmds ((eq (span-property gspan 'type) 'goalsave) (setq nestedundos @@ -1480,7 +1481,7 @@ With ARG, turn on scripting iff ARG is positive." gspan (or (eq (span-property gspan 'type) 'comment) - (eq (span-property gspan 'type) 'proverproc) ;; NB: not necess currently + ;;(eq (span-property gspan 'type) 'proverproc) ;; NB: not necess currently (and (setq ncmd (span-property gspan 'cmd)) (not (funcall proof-goal-command-p (setq cmd ncmd))) |