   "Face used for universe levels and variables"
   :group 'fstar)
 
-(defun fstar-subexpr-pre-matcher (rewind-to &optional bound-to)
-  "Move past REWIND-TO th group, then return end of BOUND-TO th."
-  (goto-char (match-end rewind-to))
-  (match-end (or bound-to 0)))
+(defface fstar-operator-face
+  '((t :inherit font-lock-variable-name-face))
+  "Face used for backticked infix operators."
+  :group 'fstar)
 
 (defconst fstar-syntax-id "\\_<[#']?[a-z_]\\(?:\\sw\\|\\s_\\)*\\_>")
-(defconst fstar-syntax-cs "\\_<[#']?[A-Z_]\\(?:\\sw\\|\\s_\\)*\\_>")
+(defconst fstar-syntax-cs "\\_<[#']?[A-Z]\\(?:\\sw\\|\\s_\\)*\\_>")
 
 (defconst fstar-syntax-id-with-subscript
   "\\_<[#']?_*[a-z]\\(?:[a-z0-9_']*[a-z]\\)?\\([0-9]+\\)['_]*\\_>")

       (0 'font-lock-type-face))
      (,fstar-syntax-universe
       (1 'fstar-universe-face))
      (,(concat "{\\(:" id "\\) *\\([^}]*\\)}")
       (1 'font-lock-builtin-face append)
       (2 'fstar-attribute-face append))
      (,(concat "\\_<\\(let\\(?: +rec\\)?\\|and\\)\\_>\\(\\(?: +" id "\\)?\\)")
       (1 'fstar-structure-face)
       (2 'font-lock-function-name-face))
      (,(concat "\\_<\\(type\\|kind\\)\\( +" id "\\)")

                                    (save-excursion
                                      (goto-char (match-beginning 0))
                                      (skip-syntax-backward "-")
                                      (or (and extra-check
                                               (not (funcall extra-check)))
                                          (eq (char-before) ?|) ;; | X: int
                                          (save-match-data
                                            ;; val x : Y:int
                                            (re-search-forward "\\_<\\(val\\|let\\|type\\)\\_>"
