             (fstar-subp--column-number-at-pos pos))))
 
 (defconst fstar-subp--info-response-regex
-  "^(defined at \\(.+?\\)(\\([0-9]+\\),\\([0-9]+\\)-\\([0-9]+\\),\\([0-9]+\\)))")
-
-(cl-defstruct fstar-pos-info
-  source-file def-start def-end type)
+  "^(defined at \\(.+?\\)(\\([0-9]+\\),\\([0-9]+\\)-\\([0-9]+\\),\\([0-9]+\\))) *\\([^ ]+\\) *: +")
+
+(cl-defstruct fstar-symbol-info
+  source-file name def-start def-end type doc)
+
+(defun fstar-symbol-info-sig (info &optional help-kbd)
+  "Format signature of INFO.
+When HELP-KBD is non nil and info includes a docstring, suggest
+to use HELP-KBD to show documentation."
+  (concat
+   (fstar-highlight-string
+    (format "%s: %s" (fstar-symbol-info-name info) (fstar-symbol-info-type info)))
+   (if (and help-kbd (fstar-symbol-info-doc info))
+       (substitute-command-keys (format " (%s for help)" help-kbd))
+     "")))
+
+(defun fstar-subp--parse-info (response)
+  "Parse info structure from RESPONSE."
+  (when (string-match fstar-subp--info-response-regex response)
+    (pcase-let* ((type-doc (substring response (match-end 0)))
+                 (`(,file ,start-r ,start-c ,end-r ,end-c ,name)
+                  (mapcar #'fstar--string-trim
+                          (fstar--match-strings-no-properties
+                           '(1 2 3 4 5 6) response)))
+                 (`(,type ,doc)
+                  (mapcar #'fstar--string-trim
+                          (if (string-match "#doc " type-doc)
+                              (list (substring type-doc 0 (match-beginning 0))
+                                    (substring type-doc (match-end 0)))
+                            (list type-doc nil)))))
+      (make-fstar-symbol-info
+       :source-file file
+       :name name
+       :def-start (cons (string-to-number start-r) (string-to-number start-c))
+       :def-end (cons (string-to-number end-r) (string-to-number end-c))
+       :type type
+       :doc doc))))
 
 (defun fstar-subp--info-continuation (continuation pos success response)
   "Handle the results (SUCCESS and RESPONSE) of an #info query at POS.
 If response is valid, forward results to CONTINUATION.  With nil
 POS, this function can also handle results of position-less #info queries."
-  (if (and success
-           (or (null pos) (eq (point) pos)) ;; Point didn't move since request
-           (string-match fstar-subp--info-response-regex response))
-      (funcall continuation
-               (make-fstar-pos-info
-                :source-file (match-string 1 response)
-                :def-start (cons (string-to-number (match-string 2 response))
-                                 (string-to-number (match-string 3 response)))
-                :def-end (cons (string-to-number (match-string 4 response))
-                               (string-to-number (match-string 5 response)))
-                :type (string-trim (substring response (match-end 0)))))
+  (if-let* ((success success)
+            (point-did-not-move (or (null pos) (eq (point) pos)))
+            (info (fstar-subp--parse-info response)))
+      (funcall continuation info)
     (funcall continuation nil)))
 
 (defun fstar--eldoc-continuation (continuation info)
   "Pass highlighted type information from INFO to CONTINUATION."
   (when info
-    (funcall continuation (fstar-highlight-string (fstar-pos-info-type info)))))
+    (funcall continuation (fstar-symbol-info-sig info "\\[fstar-doc-at-point]"))))
 
 (defun fstar--eldoc-function ()
   "Compute an eldoc string for current point.

(defun fstar-subp-killed ()
  "Clean up current source buffer."
  (fstar-subp-with-process-buffer fstar-subp--process
    (let ((leftovers (string-trim (buffer-string))))
      (unless (equal leftovers "")
        (message "F* subprocess died early: %s" leftovers)))
    (kill-buffer))

       (fstar-subp-company-candidates arg))
      (`meta
       `(:async . ,(apply-partially #'fstar-subp-company--async-meta arg)))
      (`doc-buffer
       `(:async . ,(apply-partially #'fstar-subp-company--async-doc-buffer arg)))
      (`location
       `(:async . ,(apply-partially #'fstar-subp-company--async-location arg)))
      (`sorted t)
