The Coq mailing list

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

Wilayat Khan 
<wilayatk AT gmail.com>
 writes:

   The Coq programs (files) are dependent on each other. How can I execute a
   single program (say x1.v) in Coq? I want to open a file in Coqide and
   compile line by line to understand it, but it gives errors as there are

Note that Proof General does the necessary compilation for you in
the background when you process the script step by step. See
Section 10.2 in the user manual
(http://proofgeneral.inf.ed.ac.uk/userman).

Unfortunately, I don't know if this works on Windows.

Bye,

Hendrik