       (fstar-subp-highlight-issues local-issues overlay)
       (display-local-help))))
 
+;;; ;; Visiting related errors
+
+(defun fstar-jump-to-related-error (&optional display-action)
+  "Jump to secondary error location of error at point.
+DISPLAY-ACTION is nil, `window', or `frame'."
+  (interactive)
+  (-if-let* ((loc (car (fstar-subp--alt-locs-at (point)))))
+      (fstar--navigate-to (fstar-location-filename loc)
+                     (fstar-location-line-from loc)
+                     (fstar-location-col-from loc)
+                     display-action)
+    (if (fstar-subp--in-issue-p (point))
+        (user-error "No secondary locations for this issue")
+      (user-error "No error here"))))
+
+(defun fstar-jump-to-related-error-other-window ()
+  "Jump to secondary location of error at point in new window."
+  (interactive)
+  (fstar-jump-to-related-error 'window))
+
+(defun fstar-jump-to-related-error-other-frame ()
+  "Jump to secondary location of error at point in new frame."
+  (interactive)
+  (fstar-jump-to-related-error 'frame))
 
 ;;; ;; Tracking and updating overlays
 

  (interactive)
  (mapc #'fstar--hide-buffer fstar--all-temp-buffer-names))

;;; Interactive proofs (fstar-subp)

(cl-defstruct fstar-subp-query

    (save-excursion
      (goto-char (point-max))
      (fstar-subp-advance-or-retract-to-point arg))))

;;; ;; Features based on subp

