From 2fafa16d69106aac0338b96e2a8db894d93764e9 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 30 Nov 2009 23:19:15 +0000
Subject: Replace proof-locked-end -> proof-unprocessed-begin

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

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 0101ce04..c7b8bebf 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -291,7 +291,7 @@ 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-locked-end) 1) 'type)
+    (span-at (- (proof-unprocessed-begin) 1) 'type)
     )
   )
 
@@ -1298,7 +1298,7 @@ buffer."
       (let ((pos (car mtch))
             (lgth (cadr mtch)))
         (set-buffer proof-script-buffer)
-        (goto-char (+ (proof-locked-end) 1))
+        (goto-char (+ (proof-unprocessed-begin) 1))
         (coq-find-real-start)
 
         ; utf8 adaptation is made in coq-get-last-error-location above
-- 
cgit v1.2.3