   :type '(repeat string)
   :safe #'fstar-subp-prover-args-safe-p)
 
+(defcustom fstar-subp-prover-additional-args nil
+  "Additional arguments to pass to F* in interactive mode.
+
+See `fstar-subp-prover-args' for documentation about the format
+of this variable.  Flags derived from this one are added after
+flags derived from `fstar-subp-prover-args'.
+
+This is mostly useful when working on a project that requires a
+specific value of `fstar-subp-prover-args' (typically a function)."
+  :group 'fstar
+  :type '(repeat string))
+
 (defun fstar-subp-find-fstar ()
   "Find path to F* executable."
   (fstar-find-executable fstar-executable "F*" 'fstar-executable))

  (equal args 'fstar-subp-prover-args-for-compiler-hacking))

(defcustom fstar-subp-prover-args nil
  "Used for computing arguments to pass to F* in interactive mode.

If set to a string, that string is considered to be a single
argument to pass to F*.  If set to a list of strings, each element

Some examples (see below about `…'):

- (setq fstar-subp-prover-args \"--ab\") results in F* being
called as ‘fstar.exe … --ab …’.

- (setq fstar-subp-prover-args \\='(\"--ab\" \"--cd\")) results in
F* being called as ‘fstar.exe … --ab --cd …’.

- (setq fstar-subp-prover-args (lambda () \\='(\"--ab\" \"--cd\")))
results in F* being called as ‘fstar.exe … --ab --cd …’.

In addition to these flags, `fstar-mode' always includes (as
indicated above by the first `…') both \\='--smt <path-to-z3>\\='
and one of \\='--ide\\=' and \\='--in\\=', and any flags computed
from `fstar-subp-prover-additional-args' (as indicated above by
the second `…').

To debug unexpected behaviors with this variable, try
evaluating (fstar-subp-get-prover-args).  Note that passing
