The Coq mailing list

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

This feature of proofgeneral is not implemented for coq. I would even
encourage to retract a buffer before starting a new one. The usual way
of dealing with several files is to compile modified modules when you
want to require them. Using make (use option -C dir if makefile is in
another directory) is of course useful.

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

Regards,
Pierre Courtieu

2010/12/2 Hendrik Tews 
<tews AT os.inf.tu-dresden.de>:
> Hi,
>
> the documentation of Proof General claims [1] that one can switch
> between several files in the development and that Proof General
> will maintain consistency.
>
> When I try I see the contrary: "Require Import a." fails in b.v
> until I manually compile a.v. Even worse, if I change a.v and go
> back to b.v, then Proof General reminds me to save a.v, but
> nobody takes care of compiling it!
>
> Coqide shows the same behavior in this respect.
>
> Am I doing something wrong? How do other people manage coq
> projects with more than one file?
>
> Bye,
>
> Hendrik
>
> [1] 
> http://proofgeneral.inf.ed.ac.uk/htmlshow.php?title=Proof+General+user+manual&file=releases%2FProofGeneral%2Fdoc%2FProofGeneral%2FProofGeneral_4.html#Switching-between-proof-scripts
>