The Coq mailing list

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

Adam Chlipala 
<adamc AT csail.mit.edu>
 writes:

   On this subject, I recommend Section 16.4 of CPDT:
       http://adam.chlipala.net/cpdt/

Section 16.4 is slightly outdated. For Proof General, load path
elements should be configured in coq-load-path. Eg

(*** Local Variables: ***)
(*** coq-load-path: ("dir_a" ("dir_b" "path_b")) ***)
(*** End: ***)

for -I dir_a -R dir_b -as path_b . 

There should be no need to touch coq-prog-args.

For projects without ML modules simply check menu Coq -> Settings
-> Compile Before Require and forget about Makefiles. As I wrote
before, the details are in Section 10.2 of the user manual
(http://proofgeneral.inf.ed.ac.uk/userman).

Bye,

Hendrik