 ;; * Syntax highlighting
 ;; * Unicode math (prettify-symbols-mode)
 ;; * Documentation and search
-;; * Simple indentation
+;; * Relative indentation
 ;; * Type hints (Eldoc)
 ;; * Autocompletion (Company)
 ;; * Type-aware snippets (Yasnippet)

(defconst fstar-known-modules
  '((font-lock        . "Syntax highlighting")
    (prettify         . "Unicode math (e.g. display forall as ∀; requires emacs 24.4 or later)")
    (indentation      . "Indentation (based on control points)")
    (comments         . "Comment syntax and special comments ('(***', '(*+', etc.)")
    (flycheck         . "Real-time verification with Flycheck")
    (interactive      . "Interactive verification (à la Proof-General)")

    (setq prompt (format prompt default-info)))
  (read-string prompt nil nil default))

(defun fstar-in-comment-p (&optional pos)
  "Return non-nil if POS is inside a comment."
  (nth 4 (syntax-ppss pos)))

(defun fstar--column-in-commment-p (column)
  "Return non-nil if point at COLUMN is inside a comment."
  (save-excursion
    (move-to-column column)
    (fstar-in-comment-p)))

(defun fstar-subp--column-number-at-pos (pos)
  "Return column number at POS."
