       (funcall fn-or-v)
     fn-or-v))
 
+(defun fstar--remote-p ()
+  "Check if current buffer is remote."
+  (and buffer-file-name (tramp-tramp-file-p buffer-file-name)))
+
+(defun fstar--maybe-cygpath (path)
+  "Translate PATH using Cygpath if appropriate."
+  (if (and (eq system-type 'cygwin) (not (fstar--remote-p)))
+      (string-trim-right (car (process-lines "cygpath" "-w" path)))
+    path))
+
 ;;; Debugging
 
 (defvar fstar-debug nil

      (let* ((buf (fstar-subp-make-buffer))
             (process-connection-type nil)
             (tramp-process-connection-type nil)
             (args (fstar--subp-get-prover-args))
             (proc (fstar--subp-start-process buf f*-abs args)))
        (fstar-log 'info "Started F* interactive: %S" (cons f*-abs args))
        (set-process-query-on-exit-flag proc nil)
        (set-process-filter proc #'fstar-subp-filter)


(defun fstar-subp--overlay-legend-help-function (fn help-string)
  "Show legend of overlay statuses in buffer indicated by HELP-STRING.
If HELP-STRING doesn't have `fstar-subp--legend' property, call
FN instead."
  (-if-let* ((buf (and help-string
                       (get-text-property 0 'fstar-subp--legend help-string))))
      (when (buffer-live-p buf)
        (with-current-buffer buf
          (fstar-subp--show-overlay-legend-mode-line)))
