 into blocks; process it as one large block instead."
   (interactive "P")
   (fstar-subp-start)
-  (cond
-   ((fstar-subp--in-tracked-region-p)
-    (fstar-subp-retract-until (point)))
-   ((consp arg)
-    (fstar-subp-enqueue-until (point)))
-   (t
-    (fstar-subp-advance-until (point)))))
+  (fstar--widened
+    (cond
+     ((fstar-subp--in-tracked-region-p)
+      (fstar-subp-retract-until (point)))
+     ((consp arg)
+      (fstar-subp-enqueue-until (point)))
+     (t
+      (fstar-subp-advance-until (point))))))
 
 (defun fstar-subp-advance-or-retract-to-point-lax (&optional arg)
   "Like `fstar-subp-advance-or-retract-to-point' with ARG, in lax mode."

  "Retract everything and process (possibly in LAX mode) again to POS."
  (interactive (list (point) (not (null current-prefix-arg))))
  (fstar-subp-start)
  (fstar-subp-retract-until (point-min))
  (let ((fstar-subp--lax lax))
    (fstar-subp-advance-until pos)))

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

Pass ARG to `fstar-subp-advance-or-retract-to-point'."
  (interactive "P")
  (let ((fstar-subp--lax t))
    (fstar--widened-excursion
      (goto-char (point-max))
      (fstar-subp-advance-or-retract-to-point arg))))

