 
 (defun fstar-setup-font-lock ()
   "Setup font-lock for use with F*."
+  (font-lock-mode)
   (setq-local
    font-lock-defaults
    `(((,fstar-syntax-constants    . 'font-lock-constant-face)


;;; Comment syntax

(defun fstar-syntactic-face-function-aux (_ _b _c in-string comment-depth _d _e _f comment-start-pos _g)
  "Choose face to display.

Arguments IN-STRING COMMENT-DEPTH and COMMENT-START-POS ar as in
`font-lock-syntactic-face-function'."
  (cond (in-string font-lock-string-face)
        ((and comment-depth
              comment-start-pos
              (numberp comment-depth))
         (save-excursion
           (goto-char comment-start-pos)
           (cond


(defun fstar-setup-comments ()
  "Set comment-related variables for F*."
  (setq-local comment-start      "//")
  (setq-local comment-end        "")
  (setq-local comment-start-skip "\\s-*\\((\\*+\\|//\\)\\s-*")
  (setq-local comment-end-skip   "\\s-*\\*+)\\s-*")
  (setq-local font-lock-syntactic-face-function #'fstar-syntactic-face-function))

