aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq.el')
-rw-r--r--coq/coq.el9
1 files changed, 2 insertions, 7 deletions
diff --git a/coq/coq.el b/coq/coq.el
index 6c59bda7..2c048ad5 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1210,15 +1210,10 @@ properly unlock ANCESTOR-SRC on retract."
(defun coq-unlock-ancestor (ancestor-src)
"Unlock ANCESTOR-SRC."
- (let* ((true-ancestor (file-truename ancestor-src))
- (buffer (find-buffer-visiting true-ancestor)))
- ;(message "unlock %s in buf %s" ancestor-src buffer)
+ (let* ((true-ancestor (file-truename ancestor-src)))
(setq proof-included-files-list
(delete true-ancestor proof-included-files-list))
- (if buffer
- (with-current-buffer buffer
- (proof-set-locked-end (point-min))
- (proof-script-delete-spans (point-min) (point-max))))))
+ (proof-restart-buffers (proof-files-to-buffers (list true-ancestor)))))
(defun coq-unlock-all-ancestors-of-span (span)
"Unlock all ancestors that have been locked when SPAN was asserted."