   (fstar-assert (memq status fstar-subp-statuses))
   (let* ((inhibit-read-only t)
          (lax (overlay-get overlay 'fstar-subp--lax))
-         (help-echo (propertize " " 'fstar--subp-legend (current-buffer))))
+         (help-echo (propertize " " 'fstar-subp--legend (current-buffer))))
     (overlay-put overlay 'fstar-subp-status status)
     (overlay-put overlay 'priority -1)
     (overlay-put overlay 'help-echo help-echo)

;; * Snippets (Yasnippet)
;; * Interactive proofs (à la Proof-General)
;; * Whole-buffer verification (Flycheck)
;;
;; See https://github.com/FStarLang/fstar-mode.el for setup and usage tips.


          (t (user-error "Interpreting `fstar-subp-prover-args' \
led to invalid value [%s]" args)))))

(defun fstar-subp--get-prover-args ()
  "Compute F*'s arguments."
  (let ((smt-path (fstar--maybe-cygpath (fstar-subp-find-smt-solver)))
        (usr-args (fstar-subp--parse-prover-args)))
    `(,(fstar-subp--buffer-file-name) "--in" "--smt" ,smt-path ,@usr-args)))

(defun fstar-subp--buffer-file-name ()
  "Find name of current buffer, as sent to F*."
  (if (fstar--remote-p)
      (tramp-file-name-localname
       (tramp-dissect-file-name buffer-file-name))
    (fstar--maybe-cygpath buffer-file-name)))

(defun fstar-subp--start-process (buf prog args)
  "Start an F* subprocess PROG in BUF with ARGS."
  (apply #'start-file-process "F* interactive" buf prog args))

