The Coq mailing list

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

Hello,

coq-load-path is not a function, it is a variable that you can
configure (in general or locally to each buffer). It contains all
paths that should be added to coqtop path (using -I <path> options).

It is also used by the option "coq -> settings -> compile before
require" (by Hendrik Tews) to enhance the way proofgeneral deals with
"require" commands (by automatically recompiling what must be, very
useful).

You can configure globally by this command in your .emacs:

(setq coq-load-path '("/my/path" "/my/other/path"))

then these paths will be added to *all* your coq session, whatever the
file your are editing, or you can set it "file by file" by putting
this at the of each file:


(*
*** Local Variables: ***
*** coq-load-path: ("." "./foo") ***
*** End: ***
 *)


there are other variables of the same kind, like coq-prog-args (that
should not contain -I options).

Best regards,
Pierre Courtieu



2011/11/15 Victor Porton 
<porton AT narod.ru>:
> How to set Proof General load path?
>
> coq-load-path interactive function is mentioned on the Web but is missing 
> in my ProofGeneral-4.2pre111017.
>
> --
> Victor Porton - http://portonvictor.org
>