   "Return non-nil if OVERLAY is an fstar-subp issue overlay."
   (overlay-get overlay 'fstar-subp-issue))
 
-(defun fstar-subp-issues-overlays ()
+(defun fstar-subp-issue-overlays ()
   "Find all -subp issues overlays in the current buffer."
-  (cl-loop for overlay being the overlays of (current-buffer)
-           when (fstar-subp-issue-overlay-p overlay)
-           collect overlay))
+  (-filter #'fstar-subp-issue-overlay-p (overlays-in (point-min) (point-max))))
+
+(defun fstar-subp-issue-overlays-at (pt)
+  "Find all -subp issues overlays at point PT."
+  (-filter #'fstar-subp-issue-overlay-p (overlays-at pt t)))
 
 (defun fstar-in-comment-p ()
   "Return non-nil if point is inside a comment."

                            (fstar-issue-col-to issue)))
         (overlay (make-overlay from (max to (1+ from)) (current-buffer) t nil)))
    (overlay-put overlay 'fstar-subp-issue t)
    (overlay-put overlay 'face 'fstar-subp-overlay-issue-face)
    (overlay-put overlay 'help-echo (fstar-issue-message issue))
    (overlay-put overlay 'modification-hooks '(fstar-subp-remove-issue-overlay))
    (when (fboundp 'pulse-momentary-highlight-region)
      (pulse-momentary-highlight-region from to))))

(defun fstar-subp-highlight-issues (issues)
  "Highlight ISSUES whose name match that of the current buffer."
  (fstar-assert issues)
  (mapcar #'fstar-subp-highlight-issue issues))

(defun fstar-subp-jump-to-issue (issue)


(defun fstar-subp-remove-issues-overlays ()
  "Remove all F* overlays in the current buffer."
  (mapcar #'delete-overlay (fstar-subp-issue-overlays)))

(defun fstar-subp-find-response (proc)
  "Find full response in PROC's buffer; handle it if found."
