The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

Hi,

the new implementation of multiple file support for Coq in Proof
General comes close to completion, see
http://askra.de/software/multiple-coq/ . However, because of
internal changes the old option coq-auto-compile-vos is not
working any more (and this is not trivial to fix).

Therefore I would like to ask if there are people who would miss
coq-auto-compile-vos in the new Proof General version. 

Strictly speaking the option coq-auto-compile-vos is not
necessary any more. Whenever Proof General processes a Require
command, it now compiles the necessary files before sending the
Require to coqtop. However, coq-auto-compile-vos might be
interesting for those who prefer the compilation to happen when
they leave a fully processed buffer. 

Please reply to me, if you would miss coq-auto-compile-vos in the
next Proof General release.

Bye,

Hendrik