       (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))
       (let ((linum (1- (line-number-at-pos (overlay-start ov)))))

  (when (fstar--lispify-null defined-at)
    (let-alist defined-at
      (make-fstar-location
       :filename .fname
       :line-from (elt .beg 0)
       :col-from (elt .beg 1)
       :line-to (elt .end 0)

`window' means in a side window."
  (-if-let* ((def-loc (and (fstar-lookup-result-p info)
                           (fstar-lookup-result-def-loc info))))
      (fstar--navigate-to def-loc display-action)
    (message "No definition found")))

(defun fstar-jump-to-definition-1 (pos disp)
