   (let ((beg (fstar-subp-unprocessed-beginning))
         (end (fstar-skip-spaces-backwards-from end)))
     (fstar-assert (cl-loop for overlay in (overlays-in beg end)
-                       never (fstar-subp-tracking-overlay-p overlay)))
+                      never (fstar-subp-tracking-overlay-p overlay)))
     (if (<= end beg)
         (unless no-error
           (user-error "Nothing more to process!"))

(defun fstar-subp-jump-to-issue (issue)
  "Jump to ISSUE in current buffer."
  (goto-char (fstar-issue-offset (fstar-issue-line-from issue)
                             (fstar-issue-col-from issue))))

(defun fstar-subp-handle-failure (response overlay)
  "Process failure RESPONSE from F* subprocess for OVERLAY."

;;; Prettify symbols

(defconst fstar-symbols-alist '(("exists" . ?∃) ("forall" . ?∀) ("fun" . ?λ)
                           ("nat" . ?ℕ) ("int" . ?ℤ)
                           ("True" . ?⊤) ("False" . ?⊥)
                           ("*" . ?×) ("~>" . ?↝)
                           ("<=" . ?≤) (">=" . ?≥) ("::" . ?⸬)
                           ("/\\" . ?∧) ("\\/" . ?∨) ("~" . ?¬) ("<>" . ?≠)
                           ;; ("&&" . ?∧) ("||" . ?∨) ("=!=" . ?≠)
                           ("<==>" . ?⟺) ("==>" . ?⟹)
                           ("=>" . ?⇒) ("->" . ?→)
                           ;; ("(|" . 10629) ("|)" . 10630)
                           ("'a" . ?α) ("'b" . ?β) ("'c" . ?γ)
                           ("'d" . ?δ) ("'e" . ?ϵ))
  "Fstar symbols.")

(defun fstar-setup-prettify ()
