   "Remove OVERLAY."
   (delete-overlay overlay))
 
+(defconst fstar-subp--related-location-help-string-1
+  (format "\\[fstar-jump-to-related-error] to visit, %s to come back"
+          (if (fboundp 'xref-pop-marker-stack)
+              "\\[xref-pop-marker-stack]" "\\[pop-global-mark]")))
+
 (defun fstar-subp--related-location-help-string ()
   "Build a string describing motion commands for related locations."
-  (substitute-command-keys
-   "\\[fstar-jump-to-related-error] to visit, \\[pop-global-mark] to come back"))
+  (substitute-command-keys fstar-subp--related-location-help-string-1))
 
 (defun fstar-subp--help-echo-for-alt-locs (locs)
   "Prepare a string describing LOCS and how to browse to them."

                   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--fixup-location (loc)
  "Destructively replace <input> with the name of the current buffer in LOC."
  (cl-typecase loc
    (fstar-location (when (equal (fstar-location-filename loc) "<input>")
                 (fstar-assert buffer-file-name) ;; FIXME "unknown"
                 (setf (fstar-location-filename loc) buffer-file-name))))
  loc)

(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
    (fstar-subp--fixup-location loc)
    ;; Adjust line numbers
    (unless (or (fstar--has-feature 'absolute-linums-in-errors) (null ov))

      (pcase-let* ((`(,fname ,line ,offset)
                    (cl-etypecase def-loc
                      (string `(,def-loc ,1 ,(point-min)))
                      (fstar-location `(,(fstar-location-remote-filename def-loc)
                                   ,(fstar-location-line-from def-loc)
                                   ,(fstar-location-beg-offset def-loc))))))
        (funcall callback (if (string= fname "<input>")
