The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

> (*
> *** Local Variables: ***
> *** coq-prog-name: "...." ***
> *** coq-prog-args: ("-emacs-U" "-impredicative-set")***
> *** End: ***
>  *)
> If one works with several files at the same time the PG applies the
> arguments, it seems, which are set in the first of the files loaded.
> Vladimir.

Hi,

More precisely, it applies the arguments present in the buffer in
which you *started* coq. If you want to start coq again for a file
with different arguments, you need to kill coq (C-c C-x or Coq > Exit
Coq) before scripting the new file.

<ad>
Notice that coq-prog-args use to be the place to also put "-I" options
but there is another way to set coq load path in trunk version of pg:

*** coq-load-path: ("/my/coq/dir/lib" "the/other/one") ***

This (experimental) mechanism, due to Hendrik Tews, allows pg to check
and recompile automatically modified dependencies when scripting a
"Require".
</ad>

Cheers,
Pierre Courtieu