From 0f35c852e109ab3ea9dbadd00318574aecdfcfa9 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 10 Oct 2010 16:18:43 +0000
Subject: coq-find-and-forget: Allow undoing prover processed regions (i.e.
 files locked by Require).  Some progress towards #363, and at least stops an
 ugly type error when a Require'd file is retracted.

---
 coq/coq.el | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/coq/coq.el b/coq/coq.el
index b489dd95..bc76761e 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -395,6 +395,10 @@ If locked span already has a state number, then do nothing. Also updates
 
 (defun coq-find-and-forget (span)
   "Backtrack to SPAN.  Using the \"Backtrack n m p\" coq command."
+  (if (eq (span-property span 'type) 'proverproc)
+      ;; processed externally (i.e. Require, etc), nothing to do
+      ;; (should really be unlocked when we undo the Require).
+      nil 
   (let* (ans (naborts 0) (nundos 0)
              (proofdepth (coq-get-span-proofnum span))
              (proofstack (coq-get-span-proofstack span))
@@ -411,7 +415,7 @@ If locked span already has a state number, then do nothing. Also updates
        (format "Backtrack %s %s %s . "
                (int-to-string span-staten)
                (int-to-string proofdepth)
-               naborts)))))
+               naborts))))))
 
 (defvar coq-current-goal 1
   "Last goal that Emacs looked at.")
-- 
cgit v1.2.3