 (defface fstar-literate-comment-face
   '((t :inherit default))
   "Face used for literate comments (///)."
-  :group 'fstar)
+  :group 'fstar-literate)
 
 (defface fstar-literate-gutter-face
   '((t :inverse-video t :inherit font-lock-comment-face))
   "Face used for the fringe next to literate comments (///)."
-  :group 'fstar)
+  :group 'fstar-literate)
 
 (defconst fstar-comment-start-skip "\\(//+\\|(\\*+\\)[ \t]*")
 

(defface fstar-subp-overlay-lax-face
  '((t :slant italic))
  "Face used to highlight lax-checked sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-pending-face
  '((((background light)) :background "#AD7FA8")
    (((background dark))  :background "#5C3566"))
  "Face used to highlight pending sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-pending-lax-face
  '((t :inherit (fstar-subp-overlay-pending-face fstar-subp-overlay-lax-face)))
  "Face used to highlight pending lax-checked sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-busy-face
  '((((background light)) :background "mistyrose")
    (((background dark))  :background "mediumorchid"))
  "Face used to highlight busy sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-busy-lax-face
  '((t :inherit (fstar-subp-overlay-busy-face fstar-subp-overlay-lax-face)))
  "Face used to highlight busy lax-checked sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-processed-face
  '((((background light)) :background "#EAF8FF")
    (((background dark))  :background "darkslateblue"))
  "Face used to highlight processed sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-processed-lax-face
  '((t :inherit (fstar-subp-overlay-processed-face fstar-subp-overlay-lax-face)))
  "Face used to highlight processed lax-checked sections of the buffer."
  :group 'fstar)

(defface fstar-subp-overlay-error-face
  '((t :underline (:color "red" :style wave)))
  "Face used to highlight errors."
  :group 'fstar)

(defface fstar-subp-overlay-warning-face
  '((t :underline (:color "orange" :style wave)))
  "Face used to highlight warnings."
  :group 'fstar)

(defface fstar-subp-overlay-bullet-error-face
  '((t :foreground "red"))
  "Face used to color bullets indicating error locations."
  :group 'fstar)

(defface fstar-subp-overlay-bullet-warning-face
  '((t :foreground "orange"))
  "Face used to color bullets indicating warning locations."
  :group 'fstar)

(defmacro fstar-subp-with-process-buffer (proc &rest body)
  "If PROC is non-nil, move to PROC's buffer to eval BODY."

(defface fstar-proof-state-separator-face
  '((t :inherit highlight :height 0.1))
  "Face applied to the goal line in proof states."
  :group 'fstar-tactics)

(defface fstar-proof-state-header-face
  '((t :weight bold))
  "Face applied to proof-state headers in proof states window."
  :group 'fstar-tactics)

(defface fstar-proof-state-header-timestamp-face
  '((t :inherit font-lock-comment-face))
  "Face applied to proof-state headers in proof states window."
  :group 'fstar-tactics)

(defface fstar-goal-header-face
  '((t :weight demibold))
  "Face applied to goal headers in proof states."
  :group 'fstar-tactics)

(defface fstar-hypothesis-name-face
  '((t :inherit (font-lock-variable-name-face bold)))
  "Face applied to hypothesis names in proof states."
  :group 'fstar-tactics)

(defface fstar-hypothesis-face
  '((t))
  "Face applied to hypotheses in proof states."
  :group 'fstar-tactics)

(defface fstar-goal-line-face
  '((((supports :strike-through t)) :strike-through t :height 0.5)
    (t :underline t))
  "Face applied to the goal line in proof states."
  :group 'fstar-tactics)

(defface fstar-goal-type-face
  '((t))
  "Face applied to the goal's type in proof states."
  :group 'fstar-tactics)

(defface fstar-goal-witness-face
  '((t :height 0.75 :inherit font-lock-comment-face))
  "Face applied to the goal's witness in proof states."
  :group 'fstar-tactics)

(defun fstar-tactics--insert-hyp-group (names type)
  "Insert NAMES: TYPE into current buffer."
