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.

1 files changed, 5 insertions, 1 deletions

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.")