     (dolist (opt-info options)
       (fstar-subp--list-options-1 display-default sp1 sp2 nl opt-info))))
 
-(defun fstar-subp--list-options-continuation (source-buf response)
+(defun fstar-subp--list-options-continuation (source-buf status response)
   "Let user jump to one of the dependencies in RESPONSE.
-SOURCE-BUF indicates where the query was started from."
-  (if response
+SOURCE-BUF indicates where the query was started from.  STATUS is
+the original query's status."
+  (if (eq status 'success)
       (let-alist response
         (with-help-window fstar--list-options-buffer-name
           (with-current-buffer standard-output

                        'action 'fstar--visit-link-target)
    (insert "\n")))

(defun fstar-subp--visit-dependency-continuation (source-buf response)
  "Let user jump to one of the dependencies in RESPONSE.
SOURCE-BUF indicates where the query was started from."
  (-if-let* ((deps (and response (let-alist response .loaded-dependencies)))
             (help-window-select t))
      (with-help-window fstar--visit-dependency-buffer-name
        (with-current-buffer standard-output

                (fstar-subp--pos-check-wrapper (point)
                  (apply-partially #'fstar--insert-match-continuation type))))

(defun fstar--destruct-var-continuation (from to type status response)
  "Replace FROM..TO (with TYPE) with match from RESPONSE.
STATUS is the original query's status."
  (pcase (and (eq status 'success) (split-string response "\n"))
    (`nil
     (message "No match found for type `%s'." type))
    (`(,_name ,branch)
