       (fstar-tactics--previous-proof-state (- n))
     (dotimes (_ n)
       (goto-char (point-at-eol))
-      (let ((next (next-single-char-property-change (point) 'fstar--header)))
+      (let ((next (next-single-char-property-change (point) 'fstar--proof-state)))
         (unless (eq next (point-max)) (goto-char next)))
       (goto-char (point-at-bol)))
     (recenter 0)))

    (insert "\n"))
  (fstar--insert-with-face 'fstar-proof-state-header-face
      (propertize (or (fstar-proof-state-label ps) "…")
                  'line-prefix "" 'wrap-prefix "" 'fstar--header t))
  (when (fstar-proof-state-location ps)
    (insert " @ ")
    (fstar--insert-link (fstar-proof-state-location ps) 'link 'window))

  (fstar-tactics--insert-goals (fstar-proof-state-goals ps) "Goal")
  (fstar-tactics--insert-goals (fstar-proof-state-smt-goals ps) "SMT goal"))

(defun fstar-tactics--proof-state-at-point ()
  "Read the proof state from the current point."
  (get-text-property (point) 'fstar--proof-state))

(defun fstar-tactics--next-proof-state (&optional n)
  "Go forward N goals (default: 1)."
  (interactive "^p")
