From 50dd6fc90665dd805277257b40c93380a535daa2 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 11 Jun 2002 18:05:55 +0000
Subject: 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".

---
 coq/coq.el | 14 +++++++++++---
 1 file 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)))
-- 
cgit v1.2.3