   :group 'fstar
   :type '(choice (const :tag "No Flycheck support" nil)
                  (const :tag "Whole-buffer verification (slow)" 'fstar)
-                 (const :tag "Light syntax checking (fast)" 'fstar-interactive)))
+                 (const :tag "Lightweight typechecking (fast)" 'fstar-interactive)))
 
 (make-variable-buffer-local 'fstar-flycheck-checker)
 

(defun fstar-subp-process-queue (buffer)
  "Process the next pending overlay of BUFFER, if any."
  (with-current-buffer buffer
    (fstar-subp-start)
    (setq fstar-subp--queue-timer nil)
    (unless (fstar-subp--busy-p)
      (-if-let* ((overlay (car-safe (fstar-subp-tracking-overlays 'pending))))
          (progn (fstar-log 'info "Processing queue")

(defun fstar-subp--flycheck-continuation (callback status response)
  "Forward results of Flycheck check (STATUS and RESPONSE) to CALLBACK."
  (if (eq status 'interrupted)
      (funcall callback 'interrupted nil)
    (let* ((raw-issues (fstar-subp-parse-issues response))
           (issues (mapcar #'fstar-subp-cleanup-issue raw-issues)))
      (fstar-log 'info "Highlighting Flycheck issues: %S" issues)
