                 (insert replacement)))))))
     (buffer-substring-no-properties (point-min) (point-max))))
 
-(defun fstar-subp-send-region (beg end)
+(defun fstar-subp-send-region (beg end lax)
   "Send the region between BEG and END to the inferior F* process."
   (interactive "r")
   (fstar-subp-start)
-  (let ((msg (concat fstar-subp--header
+  (let ((msg (concat (if (eq lax 0) fstar-subp--header fstar-subp--laxheader)
                      (fstar-subp-prepare-message (buffer-substring-no-properties beg end))
                      fstar-subp--footer)))
     (fstar-subp-log "QUERY [%s]" msg)

    ("C-c C-p"        "C-S-p" fstar-subp-retract-last)
    ("C-c RET"        "C-S-i" fstar-subp-advance-or-retract-to-point)
    ("C-c <C-return>" "C-S-i" fstar-subp-advance-or-retract-to-point)
    ("C-c C-x"        "C-M-c" fstar-subp-kill-one-or-many))
  "Proof-General and Atom bindings table.")


  (goto-char (fstar-subp-unprocessed-beginning))
  (fstar-subp-skip-comments-and-whitespace)
  (-if-let* ((next-start (fstar-subp-next-block-sep nil)))
      (fstar-subp-enqueue-until 0 next-start)
    (user-error "Cannot find a full block to process")))

(defun fstar-sub-overlay-contains-build-config (overlay)
