The Coq mailing list

[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