     (string
      (fstar--navigate-to-1 target display-action))
     (fstar-location
-     (fstar--navigate-to-1 (fstar-location-filename target)
+     (fstar--navigate-to-1 (fstar-location-remote-filename target)
                       (fstar-location-line-from target)
                       (fstar-location-col-from target)
                       display-action))))

    fn-or-v))

(defun fstar--remote-p ()
  "Check if current buffer is remote."
  (and buffer-file-name (tramp-tramp-file-p buffer-file-name)))

(defun fstar--maybe-cygpath (path)
  "Translate PATH using Cygpath if appropriate."
  (if (and (eq system-type 'cygwin) (not (fstar--remote-p)))
      (string-trim-right (car (process-lines "cygpath" "-w" path)))
    path))

(defun fstar--tramp-find-executable (prog)
  "Check if PROG is in the remote path."
  (let ((tramp-name (tramp-dissect-file-name buffer-file-name)))
    (tramp-find-executable tramp-name prog nil)))

(defun fstar--hide-buffer (buf)
  "Hide window displaying BUF, if any.

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

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

(defun fstar-subp--fixup-fname (fname)
  "Return FNAME, or the name of the current buffer if FNAME is <input>."
  (if (equal fname "<input>")
      (progn (fstar-assert buffer-file-name) buffer-file-name)
    fname))

(defun fstar-subp--fixup-location (loc)
  "Replace <input> with the name of the current buffer in LOC."
  (cl-typecase loc
    (fstar-location (cl-callf fstar-subp--fixup-fname (fstar-location-filename loc))))
  loc)

(defun fstar-subp-cleanup-issue (issue &optional ov)
  "Fixup ISSUE: clean up file name and adjust line numbers wrt OV."
  (dolist (loc (fstar-issue-locs issue))
    ;; Clean up file name
    (fstar-subp--fixup-location loc)
    ;; Adjust line numbers
    (unless (or (fstar--has-feature 'absolute-linums-in-errors) (null ov))
