       (fstar-tactics--insert-goal goal)
       (insert "\n"))))
 
-(defun fstar-tactics--insert-proof-state (proof-state)
-  "Dump PROOF-STATE into current buffer."
-  (let-alist proof-state
-    (unless (bobp)
-      (fstar--insert-with-face 'fstar-proof-state-separator-face
-          (propertize "\n" 'line-prefix "" 'line-height t))
-      (insert "\n"))
-    (fstar--insert-with-face 'fstar-proof-state-header-face
-        (let ((label (if (member .label '(nil "")) "…" .label)))
-          (propertize label 'line-prefix "" 'wrap-prefix "" 'fstar--header t)))
-    (let ((timestamp (current-time-string)))
-      (insert " " (fstar--specified-space-to-align-right timestamp 1))
-      (fstar--insert-with-face 'fstar-proof-state-header-timestamp-face timestamp))
-    (insert (propertize "\n" 'line-spacing 0.2))
-    (fstar-tactics--insert-goals .goals "Goal")
-    (fstar-tactics--insert-goals .smt-goals "SMT goal")))
+(defun fstar-tactics--insert-proof-state (ps)
+  "Dump proof state PS into current buffer."
+  (unless (bobp)
+    (fstar--insert-with-face 'fstar-proof-state-separator-face
+        (propertize "\n" 'line-prefix "" 'line-height t))
+    (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))
+  (let ((timestamp (current-time-string)))
+    (insert " " (fstar--specified-space-to-align-right timestamp 1))
+    (fstar--insert-with-face 'fstar-proof-state-header-timestamp-face timestamp))
+  (insert (propertize "\n" 'line-spacing 0.2))
+  (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--next-proof-state (&optional n)
   "Go forward N goals (default: 1)."

       (with-selected-window window
         (recenter 0)))))

(defun fstar-tactics--display-proof-state (proof-state)
  "Display PROOF-STATE in a separate *goals* buffer."
  (let ((help-window-select nil))
    (fstar-tactics--with-goals-buffer
      (goto-char (point-max))
      (save-excursion
        (fstar-tactics--insert-proof-state proof-state))
      (unless (bobp) (forward-line 2)))))

;;; ;; Starting the F* subprocess


;;; ;; ;; Tactics

(cl-defstruct fstar-proof-state
  label goals smt-goals)

(defconst fstar--goals-buffer-name "*fstar: goals*")
(push fstar--goals-buffer-name fstar--all-temp-buffer-names)

