                                 :col-to (string-to-number col-to)))
                       :message message)))
 
+(defun fstar-subp-json--extract-alt-locs (message)
+  "Extract secondary locations (see also, Also see) from MESSAGE.
+Returns a pair of (CLEAN-MESSAGE . LOCATIONS)."
+  (let ((locations nil))
+    (while (string-match fstar-subp--also-see-regexp message)
+      (pcase-let* ((`(,filename ,line-from ,col-from ,line-to ,col-to)
+                    (fstar--match-strings-no-properties '(1 2 3 4 5) message)))
+        (push (make-fstar-location
+               :filename filename
+               :line-from (string-to-number line-from)
+               :line-to (string-to-number line-to)
+               :col-from (string-to-number col-from)
+               :col-to (string-to-number col-to))
+              locations))
+      (setq message (replace-match "" t t message)))
+    (cons message locations)))
+
 (defun fstar-subp-json--parse-location (json)
   "Convert JSON info an fstar-mode location."
   (let-alist json

               (message (buffer-substring (match-end 0) limit))
               (`(,filename ,line-from ,col-from ,line-to ,col-to)
                (or (save-match-data
                      (when (string-match fstar-subp-legacy--also-see-regexp message)
                        (prog1 (fstar--match-strings-no-properties '(1 2 3 4 5) message)
                          (setq message (substring message 0 (match-beginning 0))))))
                    (fstar--match-strings-no-properties '(1 2 3 4 5)))))

                   collect (fstar-subp-legacy--parse-issue bound)
                   do (setq bound (match-beginning 0)))))))))

(defun fstar-subp--local-loc-p (location)
  "Check if LOCATION came from the current buffer."
  (and location
       (string= (expand-file-name buffer-file-name)
                (expand-file-name (fstar-location-filename location)))))

(defun fstar-subp-cleanup-issue (issue &optional ov)
  "Fixup ISSUE: include a file name, and adjust line numbers wrt OV."
  (dolist (loc (fstar-issue-locs issue))
    ;; Clean up file names
    (when (member (fstar-location-filename loc) '("unknown" "<input>"))
      (cl-assert buffer-file-name) ;; FIXME "unknown"
      (setf (fstar-location-filename loc) buffer-file-name))
    ;; Adjust line numbers
    (unless (or (fstar--has-feature 'absolute-linums-in-errors) (null ov))
      (let ((linum (1- (line-number-at-pos (overlay-start ov)))))
        (cl-incf (fstar-location-line-from loc) linum)
        (cl-incf (fstar-location-line-to loc) linum))))
  ;; Put local ranges first
  (let ((partitioned (-group-by #'fstar-subp--local-loc-p (fstar-issue-locs issue))))
    (setf (fstar-issue-locs issue)
          (append (cdr (assq t partitioned))
                  (cdr (assq nil partitioned)))))
  issue)

(defun fstar-subp--in-issue-p (pt)
