       (,fstar-syntax-builtins     . 'font-lock-builtin-face)
       (,fstar-syntax-preprocessor . 'font-lock-preprocessor-face)
       (,fstar-syntax-structure    . 'fstar-structure-face)
-      (,fstar-syntax-ambiguous    . 'fstar-ambiguous-face)
       ,@fstar-syntax-additional)
      nil nil))
   (font-lock-set-defaults)

                                      (skip-syntax-backward "-")
                                      (or (eq (char-before) ?|) ; | X: int
                                          (save-match-data
                                            (looking-back "\\_<val" (point-at-bol))))))))) ; val x : Y:int
    (when (and found (match-beginning 2))
      (ignore-errors
        (goto-char (match-end 2))


(defun fstar-find-subtype-annotation (bound)
  "Find {...} group between point and BOUND."
  (let ((found) (end))
    (while (and (not found) (re-search-forward "{[^:].*}" bound t))
      (setq end (save-excursion
                  (goto-char (match-beginning 0))
                  (ignore-errors (forward-sexp))
                  (point)))
      (setq found (and (<= end bound)
                       (<= end (point-at-eol))
                       (save-excursion
                         (backward-char)
                         (not (looking-at-p "[^ ]+ +with"))))))
    (when found
      (set-match-data `(,(1+ (match-beginning 0)) ,(1- end))))
    found))

(defconst fstar-syntax-additional
  (let ((id fstar-syntax-id))
    `((,fstar-syntax-cs
       (0 'font-lock-type-face))
      (,(concat "{\\(:" id "\\) *\\([^}]*\\)}")
       (1 'font-lock-builtin-face append)
       (2 'fstar-attribute-face append))
      (,(concat "\\_<\\(let\\(?: +rec\\_>\\)?\\)\\(\\(?: +" id "\\)?\\)")
       (1 'fstar-structure-face)
       (2 'font-lock-function-name-face))
      (,(concat "\\_<\\(type\\|kind\\)\\( +" id "\\)")
       (1 'fstar-structure-face)
       (2 'font-lock-function-name-face))
      (,(concat "\\_<\\(val\\) +\\(" id "\\) *:")
       (1 'fstar-structure-face)
       (2 'font-lock-function-name-face))
      (fstar-find-id-with-type
       (1 'font-lock-variable-name-face))
      (fstar-find-subtype-annotation
       (0 'fstar-subtype-face append))
      ("%\\[\\([^]]+\\)\\]"
       (1 'fstar-decreases-face append))
      ("\\_<\\(forall\\|exists\\) [^.]+\."
       (0 'font-lock-keyword-face)
       (fstar-find-id (fstar-subexpr-pre-matcher 1) nil (1 'font-lock-variable-name-face)))
      (fstar-find-fun-and-args
       (1 'font-lock-keyword-face)
       (fstar-find-id (fstar-subexpr-pre-matcher 1) nil (1 'font-lock-variable-name-face)))
      ("(\\*--\\(build-config\\)"
       (1 'font-lock-preprocessor-face prepend))
      (,fstar-syntax-ambiguous
       (0 'fstar-ambiguous-face append))
      ("[{}]"
       (0 'fstar-braces-face append))
      (,(concat "\\_<" fstar-syntax-id-unwrapped "\\(_\\)\\([0-9]+\\)\\_>")
       (1 '(face nil invisible 'fstar-subscripts) prepend)
       (2 '(face fstar-subscript-face display (raise -0.3)) append)))))
