   (when (fboundp 'xref-push-marker-stack)
     (xref-push-marker-stack)))
 
-(defun fstar--navigate-to (fname line col display-action)
+(defun fstar--navigate-to (fname line col &optional display-action)
   "Navigate to LINE, COL of FNAME.
 DISPLAY-ACTION determines where the resulting buffer is
 shown (nil for same window, `window' for a new window, and

         (type (fstar-lookup-result-type info))
         (def (fstar-lookup-result-def info))
         (name (fstar-lookup-result-name info))
         (def-loc (fstar-lookup-result-def-loc-str info))
         (title (fstar--propertize-title name))
         (subtitle (propertize def-loc 'face '(:height 0.9))))
    (save-excursion
      (insert title "\n" subtitle)
      (fstar--doc-buffer-populate-1 "Type"
        (and type (fstar-highlight-string type)))
      (fstar--doc-buffer-populate-1 "Definition"

    (insert (fstar--propertize-title title) "\n\n"))
  (dolist (fname deps)
    (insert "  ")
    (fstar--insert-link fname fname 'default)
    (insert "\n")))

(defun fstar-subp--visit-dependency-continuation (source-buf status response)
