              (2 'font-lock-function-name-face append)
              (3 'fstar-attribute-face append)))
       ("%\\[" ("%\\[\\([^]]+\\)\\]"
-               (fstar-group-pre-matcher 1 0) nil
-               (1 'fstar-decreases-face append)))
+              (fstar-group-pre-matcher 1 0) nil
+              (1 'fstar-decreases-face append)))
       (,(concat "\\_<\\(let\\(?: +rec\\)?\\)\\(\\(?: +" id "\\)?\\) +[^=]+=")
        (1 'fstar-structure-face)
        (2 'font-lock-function-name-face)
        (fstar-find-id (fstar-subexpr-pre-matcher 2) nil
-                      (1 'font-lock-variable-name-face)))
+                  (1 'font-lock-variable-name-face)))
       (fstar-find-id-with-type
        (1 'font-lock-variable-name-face))
       (,(concat "\\_<\\(type\\|kind\\)\\( +" id "\\)\\s-*$")

(defun fstar-subp-highlight-issue (issue)
  "Highlight ISSUE in current buffer."
  (let* ((from (fstar-issue-offset (fstar-issue-line-from issue)
                                   (fstar-issue-col-from issue)))
         (to (fstar-issue-offset (fstar-issue-line-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-overlay-issue-face)

  (match-end (or bound-to 0)))

(defconst fstar-syntax-id (rx symbol-start
                          (? (or "#" "'"))
                          (any "a-z_") (* (or wordchar (syntax symbol)))
                          (? "." (* (or wordchar (syntax symbol))))
                          symbol-end))

(defconst fstar-syntax-cs (rx symbol-start
                          (any "A-Z") (* (or wordchar (syntax symbol)))
                          symbol-end))

(defun fstar-find-id-with-type (bound)
  (fstar-find-id-maybe-type bound t))
