   (dolist (loc (fstar-issue-locs issue))
     ;; Clean up file names
     (when (member (fstar-location-filename loc) '("<input>"))
-      (cl-assert buffer-file-name) ;; FIXME "unknown"
+      (fstar-assert buffer-file-name) ;; FIXME "unknown"
       (setf (fstar-location-filename loc) buffer-file-name))
     ;; Adjust line numbers
     (unless (or (fstar--has-feature 'absolute-linums-in-errors) (null ov))


(defun fstar--indentation-points ()
  "Collect indentation points for current line."
  (let ((points nil)
        (in-comment (fstar-in-comment-p (point-at-bol))))
    (save-excursion
      (while (and (not (bobp)) (> (or (car points) 1) 0))
        (fstar--indentation-previous-line)
        (let ((line-points (fstar--indentation-points-before (car points))))


(defun fstar-subp--start-syntax-check (_checker callback)
  "Start a light syntax check; pass results to CALLBACK."
  (fstar--widened
    (if (fstar-subp--can-run-flycheck)
        (let ((beg (fstar-subp--untracked-beginning-position))
              (end (fstar-subp--find-point-to-process fstar-subp-flycheck-lookahead)))
          (if (and (numberp end) (< beg end))
              (fstar-subp-peek-region
               beg end 'lax ;; FIXME make configurable
               (apply-partially #'fstar-subp--flycheck-continuation callback))
            (funcall callback 'finished nil)))
      (funcall callback 'interrupted nil))))

(flycheck-define-generic-checker 'fstar-interactive
  "Flycheck checker for F*'s interactive mode.
