 (defun fstar-subp-highlight-issue (issue)
   "Highlight ISSUE in current buffer."
   (let* ((from (fstar--row-col-offset (fstar-issue-line-from issue)
-                                      (fstar-issue-col-from issue)))
+                                 (fstar-issue-col-from issue)))
          (to (fstar--row-col-offset (fstar-issue-line-to issue)
-                                    (fstar-issue-col-to issue)))
+                               (fstar-issue-col-to issue)))
          (overlay (make-overlay from (max to (1+ from)) (current-buffer) t nil)))
     (overlay-put overlay 'fstar-subp-issue t)
     (overlay-put overlay 'face (fstar-subp-issue-face issue))

;;; Prettify symbols

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

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

(defun fstar-subp--local-issue-p (issue)
  "Check if ISSUE came from the current buffer."
