          (synths      (-filter 'lean-info-synth-p      info-list))
          (coercions   (-filter 'lean-info-coercion-p   info-list))
          (identifiers (-filter 'lean-info-identifier-p info-list))
-         (symbols     (-filter 'lean-info-symbol-p     info-list)))
+         (symbols     (-filter 'lean-info-symbol-p     info-list))
+         (extras      (-filter 'lean-info-extra-p      info-list)))
     (make-lean-info-record :type       types
                            :overload   overloads
                            :synth      synths
                            :coercion   coercions
                            :identifier identifiers
                            :symbol     symbols
+                           :extra      extras
                            :nay        (lean-info-nay-p   string)
                            :stale      (lean-info-stale-p string))))
 

               (and sym (string-prefix-p (lean-info-id-symbol-body-str sym) it)))
              (lean-info-overload-names overload))
             ", ")))
    (when (and name-str type-str)
      (setq str (format "%s : %s"
                        (propertize name-str 'face 'font-lock-variable-name-face)

    (COERCION   (lean-info-coercion-pos   info))
    (IDENTIFIER (lean-info-identifier-pos info))
    (SYMBOL     (lean-info-symbol-pos     info))
    (EXTRA      (lean-info-extra-pos     info))))
(defun lean-info-line-number (info)
  (cl-first (lean-info-pos info)))
(defun lean-info-column (info)
