coq-highlight-error: use span-add-self-removing-span (highlight and removal in background)

1 files changed, 2 insertions, 5 deletions

diff --git a/coq/coq.el b/coq/coq.el
index bfc3ed4c..aa0ccec4 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1313,11 +1313,8 @@ buffer."
           
           ;; utf8 adaptation is made in coq-get-last-error-location above
           (goto-char (+ (point) pos))
-          (let* ((sp (span-make (point) (+(point) lgth))))
-            (set-span-face sp 'proof-warning-face)
-            (unwind-protect
-                (sit-for 5) ;; da: this was 20 but seemed obnoxiously long?
-              (span-delete sp))))))))
+          (span-add-self-removing-span (point) (+ (point) lgth)
+                                       'face 'proof-warning-face))))))
 
 (defun coq-highlight-error-hook ()
   (coq-highlight-error t t))