Fixed a bug of the new synchro code (coq-find-and-forget) in

coq.el. Now do not count Tactics and unsaved goal commands for "Back".

1 files changed, 11 insertions, 3 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 571b8bf6..d00c5254 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -254,9 +254,17 @@
 		 ; backable.  This negative test bets on the fact that user
 		 ; defined commands are probably backable, which is not sure at
 		 ; all. Betting on the opposite is also wrong.
-		 ((not (proof-string-match 
-			(concat "\\`\\(" coq-not-undoable-not-backable-commands-regexp	"\\)") str))
-		  (setq nbacks (+ nbacks 1)))
+		 ((and 
+			(not (coq-goal-command-p str)) ;; saved goals are catched before this point
+			(not (proof-string-match ;; now we should match all things that deal with Back
+					(concat "\\`\\(" coq-undoable-commands-regexp "\\)")
+				  str))
+			(not (proof-string-match 
+					(concat "\\`\\(" 
+							  coq-not-undoable-not-backable-commands-regexp
+							  "\\)")
+					str)))
+			(setq nbacks (+ nbacks 1)))
 		 )
 
       (setq span (next-span span 'type)))