       (fstar-subp-enqueue-until next-start)
     (user-error "Cannot find a full block to process")))
 
-(defun fstar-sub-overlay-contains-build-config (overlay)
-  "Check if OVERLAY contains a build-config header."
-  (save-excursion
-    (save-match-data
-      (goto-char (overlay-start overlay))
-      (cl-loop while (re-search-forward (regexp-quote fstar-build-config-header) (overlay-end overlay) t)
-               thereis (fstar-in-build-config-p)))))
-
 (defun fstar-subp-pop-overlay (overlay)
   "Remove overlay OVERLAY and issue the corresponding #pop command."
   (fstar-assert (fstar-subp-available-p))
-  (if (fstar-sub-overlay-contains-build-config overlay)
-      (fstar-subp-kill)
-    (fstar-subp--query fstar-subp--cancel nil))
+  (fstar-subp--query fstar-subp--cancel nil)
   (delete-overlay overlay))
 
 (defun fstar-subp-retract-one (overlay)

  "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))))

    (goto-char (point-min))
    (let (start)
      (while (setq start (comment-search-forward nil t))
        (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)
