     (goto-char (point-min))
     (let (start)
       (while (setq start (comment-search-forward nil t))
-        (let ((skip (fstar-in-build-config-p)))
-          (goto-char start)
-          (forward-comment 1)
-          (unless skip ;; FIXME is this still needed?
-            (save-match-data
-              (let* ((comment (buffer-substring-no-properties start (point)))
-                     (replacement (replace-regexp-in-string "." " " comment t t)))
-                (delete-region start (point))
-                (insert replacement)))))))
+        (goto-char start)
+        (forward-comment 1)
+        (save-match-data ;; FIXME do we still need to strip comments?
+          (let* ((comment (buffer-substring-no-properties start (point)))
+                 (replacement (replace-regexp-in-string "." " " comment t t)))
+            (delete-region start (point))
+            (insert replacement)))))
     (buffer-substring-no-properties (point-min) (point-max))))
 
 (defun fstar-subp--push-header (pos lax)

  "Return non-nil if point is inside a comment."
  (nth 4 (syntax-ppss)))

(defun fstar-in-build-config-p ()
  "Return non-nil if point is in build config comment."
  (let ((state (syntax-ppss)))
    (and (nth 4 state)
         (save-excursion
           (goto-char (nth 8 state))
           (looking-at-p (regexp-quote fstar-build-config-header))))))

(defun fstar-subp--column-number-at-pos (pos)
  "Return column number at POS."
  (save-excursion (goto-char pos) (- (point) (point-at-bol))))

           (save-excursion
             (goto-char comment-start-pos)
             (cond
              ((looking-at (regexp-quote "(*** ")) '(:inherit font-lock-doc-face :height 2.5))
              ((looking-at (regexp-quote "(**+ ")) '(:inherit font-lock-doc-face :height 1.8))
              ((looking-at (regexp-quote "(**! ")) '(:inherit font-lock-doc-face :height 1.5))
