     (cond
      ((<= (point) limit) (fstar-subp-retract-until (point)))
      ((>  (point) limit) (if (consp arg)
-                             (fstar-subp-enqueue-until 0 (point))
-                           (fstar-subp-advance-until 0 (point)))))))
-
-;;AR: this is copy of the function above, ideally we should pass an argument, but could not make it work
+                             (fstar-subp-enqueue-until (point))
+                           (fstar-subp-advance-until (point)))))))
+
 (defun fstar-subp-advance-or-retract-to-point-lax (&optional arg)
-  "Advance or retract proof state to reach point.
-
-With prefix argument ARG, when advancing, do not split region
-into blocks; process it as one large block instead."
+  "Like `fstar-subp-advance-or-retract-to-point' with ARG, in lax mode."
   (interactive "P")
-  (fstar-subp-start)
-  (let ((limit (fstar-subp-unprocessed-beginning)))
-    (cond
-     ((<= (point) limit) (fstar-subp-retract-until (point)))
-     ((>  (point) limit) (if (consp arg)
-                             (fstar-subp-enqueue-until 1 (point))
-                           (fstar-subp-advance-until 1 (point)))))))
+  (let ((fstar-subp--lax t))
+    (fstar-subp-advance-or-retract-to-point arg)))
 
 (defconst fstar-subp-keybindings-table
   '(("C-c C-n"        "C-S-n" fstar-subp-advance-next)

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


           when (> (overlay-end overlay) pos) ;; End point is not inclusive
           do (fstar-subp-retract-one overlay)))

(defun fstar-subp-advance-until (pos)
  "Submit or retract blocks to/from prover until POS."
  (fstar-subp-start)
  (save-excursion
    (goto-char (fstar-subp-unprocessed-beginning))
    (let ((found (cl-loop do (fstar-subp-skip-comments-and-whitespace)
                          while (and (< (point) pos) (fstar-subp-next-block-sep pos))
                          do (fstar-subp-enqueue-until (point))
                          collect (point))))
      (fstar-subp-enqueue-until pos found))))

(defun fstar-subp-advance-or-retract-to-point (&optional arg)
  "Advance or retract proof state to reach point.
