From 8dedd5415de018e4ff901faec0fd5e3f02d24781 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 1 Jul 2010 21:15:44 +0000
Subject: proof-last-locked-span: save-excursion -> with-current-buffer to
 avoid spurious warning in Emacs 23.2

---
 coq/coq.el | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 5fdbbfb8..0375a5d4 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -289,11 +289,8 @@ used see coq-set-state-number. Initially 1 because Coq initial state has number
   )
 
 (defun proof-last-locked-span ()
-  (save-excursion ;; didn't found a way to avoid buffer switching
-    (set-buffer proof-script-buffer)
-    (span-at (- (proof-unprocessed-begin) 1) 'type)
-    )
-  )
+  (with-current-buffer proof-script-buffer
+    (span-at (- (proof-unprocessed-begin) 1) 'type)))
 
 ;; clone-buffer do not keep the current content of proof-response-buffer, so
 ;; here is my version
-- 
cgit v1.2.3