     (define-key map (kbd "M-<f12>") #'fstar-quick-peek)
     (define-key map (kbd "C-c C-s C-c") #'fstar-insert-match-dwim)
     (define-key map (kbd "C-c C-s C-e") #'fstar-eval)
+    (define-key map (kbd "C-c C-s C-s") #'fstar-quit-windows)
     map))
 
 (defun fstar-newline-and-indent (arg)

  (fstar-subp--query (fstar-subp--eval-query term)
                (apply-partially #'fstar-subp--eval-continuation term)))


;;;; xref-like features


(defun fstar-doc-at-point-dwim ()
  "Show documentation of identifier at point, if any."
  (interactive)
  (unless (and (eq last-command this-command)
               (fstar--hide-help-buffer fstar--doc-buffer-name))
    (fstar-subp--ensure-available #'user-error 'lookup/documentation)
    (fstar-subp--query (fstar-subp--positional-lookup-query (point))
                  (fstar-subp--lookup-wrapper #'fstar--doc-at-point-continuation (point)))))
