 
 (defconst fstar-syntax-constants-re
   (regexp-opt fstar-syntax-constants 'symbols))
+
+(defconst fstar-syntax-reserved-exact-re
+  (format "\\`%s\\'"
+          (regexp-opt
+           (append `("Type")
+                   fstar-syntax-headers
+                   fstar-syntax-fsdoc-keywords
+                   fstar-syntax-preprocessor
+                   fstar-syntax-qualifiers
+                   fstar-syntax-block-delims
+                   fstar-syntax-keywords
+                   fstar-syntax-builtins
+                   fstar-syntax-constants))))
 
 (defface fstar-structure-face
   '((((background light)) (:bold t))

URL `https://github.com/company-mode/company-mode/issues/654'), and
then returns an :async cons, as required by company-mode."
  (let ((retv (fstar-subp--query-and-wait
               (fstar-subp--completion-query prefix context) 0.03)))
    (pcase retv
      (`(t . (,status ,results))
       (fstar-subp-company--candidates-continuation
        context #'identity status results))
      (`(needs-callback . ,_)
       `(:async
         . ,(lambda (cb)
              (setf (cdr retv)
                    (apply-partially
                     #'fstar-subp-company--candidates-continuation context cb))))))))

(defun fstar-subp-company--post-completion (candidate)
  "Expand snippet of CANDIDATE, if any."

       (fstar-subp-company--prefix))
      (`candidates
       (fstar-subp-company-candidates arg fstar-subp-company--completion-context))
      ((guard (and arg (plist-member (text-properties-at 0 arg) command)))
       (get-text-property 0 command arg))
      (`meta
       `(:async . ,(apply-partially #'fstar-subp-company--async-meta arg)))
      (`doc-buffer
