The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Just to be clear: Below you're saying that I could give better advice, 
but the existing advice is still accurate, right?  (And it has the 
benefit of working with older Proof General versions.)

On 11/12/2012 10:21 AM, Hendrik Tews wrote:
> 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).
>