   "Jump to definition of identifier at point, if any."
   (interactive)
   (fstar-subp--ensure-available #'user-error 'lookup)
-  (fstar-subp--query (fstar-subp--positional-lookup-query (point))
-                (fstar-subp--lookup-wrapper #'fstar--jump-to-definition-continuation (point))))
+  (fstar-subp--query (fstar-subp--positional-lookup-query (point)
+                  '(defined-at))
+                (fstar-subp--lookup-wrapper
+                 #'fstar--jump-to-definition-continuation (point))))
 
 ;;;; Quick-peek
 

  "\\([^\0]+?\\)\\(?:#doc \\([^\0]+?\\)\\)?\\'")

(cl-defstruct fstar-lookup-result
  source-file name def-start def-end type doc)

(defun fstar-lookup-result-sig (info &optional help-kbd)
  "Format signature of INFO.

    (if (string= ns "") candidate
      (concat ns "." candidate))))

(defun fstar-subp-company--async-lookup (candidate fields continuation)
  "Pass info FIELDS about CANDIDATE to CONTINUATION.
If F* is busy, call CONTINUATION directly with symbol `busy'."
  (declare (indent 2))
  (if (fstar-subp-available-p)
      (fstar-subp--query
       (fstar-subp--positionless-lookup-query
           (fstar-subp-company--candidate-fqn candidate) fields)
       (fstar-subp--lookup-wrapper continuation nil))
    (funcall continuation 'busy)))

