   filename line-from line-to col-from col-to)
 
 (cl-defstruct fstar-issue
-  level loc alternate-loc message)
+  level locs message)
 
 (defconst fstar-subp-issue-location-regexp
   "\\(.*?\\)(\\([[:digit:]]+\\),\\([[:digit:]]+\\)-\\([[:digit:]]+\\),\\([[:digit:]]+\\))")


(defun fstar-subp-jump-to-issue (issue)
  "Jump to ISSUE in current buffer."
  (let ((loc (fstar-issue-loc issue)))
    (goto-char (fstar--row-col-offset (fstar-location-line-from loc)
                                 (fstar-location-col-from loc)))))

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

(defun fstar-subp-parse-and-highlight-issues (status response overlay)
  "Parse issues in RESPONSE (caused by processing OVERLAY) and display them.


(defun fstar-subp--make-flycheck-issue (issue)
  "Convert an F* ISSUE to a Flycheck issue."
  (-when-let* ((loc (car (fstar-issue-locs issue))))
    (flycheck-error-new-at
     (fstar-location-line-from loc)
     (1+ (fstar-location-col-from loc))
