From 98998e82ff24e927c77b9b110fd32aeac49b2a39 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 5 Jun 2003 11:11:17 +0000
Subject: Typo

---
 generic/proof-script.el | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'generic/proof-script.el')

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)))
-- 
cgit v1.2.3