           ;; Ensure progress
           (when (bobp) (forward-char))
           ;; Jump to next block separator
-          (fstar--search-predicated-forward
+          (fstar--re-search-predicated-forward
            #'fstar-subp--block-start-p fstar-subp-block-sep))
     (goto-char (match-beginning 1))))
 

  (fstar--comment-beginning pos)
  (forward-comment 1))

(defun fstar--search-predicated-1 (search-fn test-fn move-fn re)
  "Helper for `fstar--search-predicated'.
SEARCH-FN, TEST-FN, MOVE-FN, RE: see `fstar--search-predicated'."
  (catch 'found
    (while (funcall search-fn re nil t)
      (when (funcall test-fn)
        (throw 'found (point)))
      (unless (funcall move-fn)
        (throw 'found nil)))
    (throw 'found nil)))

(defun fstar--search-predicated (search-fn test-fn move-fn re)
  "Use SEARCH-FN to find matches of RE satisfying TEST-FN.
MOVE-FN is used to move the point when TEST-FN returns nil.
Return non-nil if RE can be found.  This function does not move
the point."
  (save-excursion
    (comment-normalize-vars)
    (and (fstar--search-predicated-1 search-fn test-fn move-fn re)
         ;; Ensure that the match is maximal when searching backwards for
         ;; e.g. \n+ in a buffer containing \n•\n
         (goto-char (match-beginning 0))

          ;; Find appropriate starting point
          (goto-char (point-at-eol))
          ;; Jump to next block separator
          (fstar--re-search-predicated-forward
           #'fstar-subp--block-end-p fstar-subp-block-sep))
    (goto-char (match-beginning 1))))

