   (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)
+      (fstar-subp-enqueue-until next-start)
     (user-error "Cannot find a full block to process")))
 
 (defun fstar-sub-overlay-contains-build-config (overlay)

  (save-excursion (goto-char pos) (current-column)))

(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* ((pushlc (concat fstar-subp--header
			 (format " %d %d"
				 (line-number-at-pos beg)
				 (column-number-at-pos beg))))
	 (header (if (eq lax 0)
		     pushlc
		   (concat pushlc " " fstar-subp--laxheader)))
	 (msg (concat header "\n"
		      (fstar-subp-prepare-message (buffer-substring-no-properties beg end))
		      fstar-subp--footer)))
    (fstar-subp-log "QUERY [%s]" msg)
    (process-send-string fstar-subp--process 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-l RET"        "C-S-l" fstar-subp-advance-or-retract-to-point-lax)
    ("C-l <C-return>" "C-S-l" fstar-subp-advance-or-retract-to-point-lax)
    ("C-c C-x"        "C-M-c" fstar-subp-kill-one-or-many))
  "Proof-General and Atom bindings table.")
