The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On 10 jan 2005, Stefan Monnier wrote:

> > Use the method  with Local Variables described in my previous mail. You
> > can specify any coqtop option (-I <path>, -impredicative-set ...).
> 
> But that doesn't work if the coqtop process is already executing from
> another Proof-General session.


Sure, you have to restart the coq process. 

Menu Coq -> exit Coq   then   Menu Coq -> start coq.


Be careful that if you modify the Local Variable section at the end of the
file (or if you create it), you have to kill the buffer and reload the file
for the variables to be updated.

Cheers,

Pierre