   "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]+\\)['_]*\\_>")

          (set-match-data `(,(car md) ,(point) ,@(cddr md))))))
    found))

(defun fstar-find-id (bound)
  "Find variable name between point and BOUND."
  (fstar-find-id-maybe-type bound nil))

(defun fstar-find-id-with-type (bound)
  "Find var:type pair between point and BOUND."
  (fstar-find-id-maybe-type bound t))

(defun fstar-find-fun-and-args (bound)
  "Find lambda expression between point and BOUND."
  (let ((found))
    (while (and (not found) (re-search-forward "\\_<fun\\_>" bound t))
      (-when-let* ((mdata (match-data))
                   (fnd   (search-forward "->" bound t))) ;;FIXME
        (set-match-data `(,(car mdata) ,(match-end 0)
                          ,@mdata))
        (setq found t)))
    found))

(defun fstar-find-subtype-annotation (bound)
  "Find {...} group between point and BOUND."

       (1 'fstar-structure-face)
       (2 'font-lock-function-name-face))
      (fstar-find-id-with-type
       (1 'font-lock-variable-name-face append))
      (fstar-find-subtype-annotation
       (0 'fstar-subtype-face append))
      ("%\\[\\([^]]+\\)\\]"
       (1 'fstar-decreases-face append))
      (fstar--find-quantifier-and-args
       (1 'font-lock-keyword-face)
       (fstar--find-formal (fstar-subexpr-pre-matcher 1) nil (1 'font-lock-variable-name-face append)))
      (fstar--find-fun-and-args
       (1 'font-lock-keyword-face)
       (fstar--find-formal (fstar-subexpr-pre-matcher 1) nil (1 'font-lock-variable-name-face append)))
      (,fstar-syntax-ambiguous
       (0 'fstar-ambiguous-face append))
      ("!"
