Skip to Content.
Sympa Menu

coq-club - [Coq-Club] poll on the coq-auto-compile-vos option in Proof General

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] poll on the coq-auto-compile-vos option in Proof General


chronological Thread 
  • From: Hendrik Tews <tews AT os.inf.tu-dresden.de>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] poll on the coq-auto-compile-vos option in Proof General
  • Date: Tue, 15 Feb 2011 12:40:32 +0100

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



Archive powered by MhonArc 2.6.16.

Top of Page