 CALLBACK is the company-mode asynchronous meta callback."
   (-if-let* ((def-loc (and (fstar-lookup-result-p info)
                            (fstar-lookup-result-def-loc info))))
-      (pcase-let* ((fname (fstar-location-filename def-loc))
-                   (line (fstar-location-line-from def-loc))
-                   (col (fstar-location-col-from def-loc)))
+      (pcase-let* ((fname (fstar-location-filename def-loc)))
         (funcall callback (if (string= fname "<input>")
                               (cons (current-buffer)
-                                    (fstar--row-col-offset line col))
-                            (cons fname line))))
+                                    (fstar-location-beg-offset def-loc))
+                            (cons fname (fstar-location-line-from def-loc)))))
     (funcall callback nil)))
 
 (defun fstar-subp-company--async-location (candidate callback)

(defun fstar-subp-jump-to-issue (issue)
  "Jump to ISSUE in current buffer."
  (-when-let* ((loc (car (fstar-issue-locs 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 any location in ISSUE came from the current buffer."

PARENT is the overlay whose processing caused this issue to be
reported."
  (-when-let* ((loc (car (fstar-issue-locs issue)))
               (from (fstar-location-beg-offset loc))
               (to (fstar-location-end-offset loc))
               (overlay (make-overlay from (max to (1+ from)) (current-buffer) t nil)))
    (overlay-put overlay 'fstar-subp-issue issue)
    (overlay-put overlay 'fstar-subp-issue-parent-overlay parent)
