 
 (defun fstar-subp-make-buffer ()
   "Create a buffer for the F* subprocess."
-  (let ((vernum fstar--vernum))
+  (let ((vernum fstar--vernum)
+        (features fstar--features))
     (with-current-buffer (generate-new-buffer
                           (format " *F* interactive for %s*" (buffer-name)))
       (add-hook 'kill-buffer-hook #'fstar-subp-buffer-killed t t)
-      (setq fstar--vernum vernum)
+      (setq fstar--vernum vernum fstar--features features)
       (buffer-disable-undo)
       (current-buffer))))
 

  (fstar-subp-remove-tracking-overlays)
  (fstar-subp--clear-continuations)
  (setq fstar--vernum nil
        fstar-subp--process nil
        fstar-subp--features nil
        fstar-subp--next-query-id 0))

(defun fstar-subp-kill ()

        (setq fstar--vernum (match-string 1 version-string))
      (message "F*: Can't parse version number from %S; assuming %s"
               version-string fstar-assumed-vernum)
      (setq fstar--vernum "unknown")))
  (let ((vernum (if (equal fstar--vernum "unknown") fstar-assumed-vernum fstar--vernum)))
    (pcase-dolist (`(,feature . ,min-version) fstar--features-min-version-alist)
      (when (version<= min-version vernum)
        (push feature fstar--features)))))

(defun fstar--has-feature (feature &optional error-fn)
  "Check if FEATURE is available in the current F*.
If not, call ERROR-FN if supplied with a relevant message."
  (or (null fstar--vernum)
      (memq feature fstar--features)
      (ignore
       (and error-fn
            (funcall error-fn "This feature isn't available \
in your version of F*.  You're running version %s" fstar--vernum)))))

;;; Flycheck

