 ;;; ;; ;; Tactics
 
 (cl-defstruct fstar-proof-state
-  label goals smt-goals)
+  label location goals smt-goals)
 
 (defconst fstar--goals-buffer-name "*fstar: goals*")
 (push fstar--goals-buffer-name fstar--all-temp-buffer-names)

  (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))

  (let-alist json
    (make-fstar-proof-state
     :label (if (equal .label "") nil .label)
     :location (fstar-subp-json--parse-location .position)
     :goals .goals
     :smt-goals .smt-goals)))

