 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)

  ;; min makes sure that we don't spill to the next line.
  (forward-char (min (- (point-at-eol) (point-at-bol)) column)))

(defun fstar--row-col-offset (line column)
  "Convert a (LINE, COLUMN) pair into a buffer offset."
  ;; LATER: This would be much easier if the interactive mode returned
  ;; an offset instead of a line an column.

(defun fstar-subp-jump-to-issue (issue)
  "Jump to ISSUE in current buffer."
  (-when-let* ((loc (car (fstar-issue-locs issue))))
    (goto-char (fstar-location-beg-offset loc))))

(defun fstar-subp--local-issue-p (issue)
  "Check if any location in ISSUE came from the current buffer."
