       (setq-local fstar-enabled-modules '(font-lock prettify))
       (fstar-mode))))
 
+(defun fstar--cleanup-type (type)
+  "Clean up TYPE."
+  (replace-regexp-in-string "\\(?:uu___:\\|[@#][0-9]+\\_>\\)" "" type t t))
+
+(defun fstar--unparens (str)
+  "Remove parentheses surrounding STR, if any."
+  (if (and (> (length str) 2)
+           (eq (aref str 0) ?\()
+           (eq (aref str (1- (length str))) ?\)))
+      (substring str 1 (- (length str) 1))
+    str))
+
 (defun fstar-highlight-string (str)
   "Highlight STR as F* code."
   (fstar--init-scratchpad)
   (with-current-buffer fstar--scratchpad
     (erase-buffer)
-    (insert str)
+    (insert (fstar--cleanup-type str))
     (if (fboundp 'font-lock-ensure)
         (font-lock-ensure)
       (with-no-warnings (font-lock-fontify-buffer)))

When HELP-KBD is non nil and info includes a docstring, suggest
to use HELP-KBD to show documentation."
  (concat
   (let* ((type (fstar-lookup-result-type info))
          (clean-type (replace-regexp-in-string "uu___:" "" type)))
     (fstar-highlight-string
      (format "%s: %s" (fstar-lookup-result-name info) clean-type)))
   (if (and help-kbd (fstar-lookup-result-doc info))
       (substitute-command-keys (format " (%s for help)" help-kbd))
     "")))

                       (if (string-match-p "\n" term) "\n" " ")
                       (fstar--reduction-arrow "↓" "βδιζ")
                       (if (string-match-p "\n" response) "\n" " ")
                       (fstar-highlight-string (fstar--unparens response))))
    (`failure (message "Evaluation of [%s] failed: %s"
                       (fstar-highlight-string term)
                       (string-trim response)))))
