   "Face used for literate comments (///)."
   :group 'fstar)
 
-(defface fstar-literate-fringe-face
+(defface fstar-literate-gutter-face
   '((t :inverse-video t :inherit font-lock-comment-face))
   "Face used for the fringe next to literate comments (///)."
   :group 'fstar)

           (save-excursion
             (goto-char comment-start-pos)
             (cond
              ((looking-at-p "///\\( \\|$\\)") 'fstar-literate-comment-face)
              ((looking-at-p "([*]\\([*][*]\\|[*] ?[*]\\)[[:space:]\n]")
               '(:inherit font-lock-doc-face :height 2.5))
              ((looking-at-p "([*]\\([*]?[+]\\|[*] ?[*][*]\\)[[:space:]\n]")

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

(defconst fstar--literate-comment-re "^///\\( \\|$\\)"
  "Regexp matching literate comment openers.")

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