The Coq mailing list

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

Pierre Courtieu 
<Pierre.Courtieu AT cnam.fr>
 writes:

   I would even
   encourage to retract a buffer before starting a new one. 

Proof General retracts partial buffers when one starts scripting
in a new one.

   By the way, does someone know how to tell make to compile all
   dependencies of target but not the target itself? This would help.

This is not too difficult. Just use a pseudo goal, which depends
on the real things. eg

buf1.pseudo: buf2.vo ...

and in buf1.v you include at the end

(*** Local Variables ***)
(*** compile-command: "make buf1.pseudo" ***)
(*** End: ***)

This causes emacs to call the indicated command when you invoke
M-x compile (which one should bind to some key).

Bye,

Hendrik