The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>]

On 06 jui 2005, Guillaume Melquiond wrote:

> Some of the command-line options of coqc work with coqide too. So you
> can just use "coqide -I .." to set the path beforehand.

-I is definitely what you need. Actually coqc works exactly like a
compiler: you need a line in your makefile like : 
COQC=coqc -I . -I foo -I bar

It is recommended (I believe) that you have only one makefile at the
root of your development (and ou call it with make -C .. when you are in
subdirectories). 

coqide and coqtop also accept the -I option. So after compiling
dependencies with make -C, then do coqtop -I <paths to dependencies>. For
example coqtop -I ../foo -I .. if you are in the bar directory.

If you use coqide, then call it directly with this options
coqide -I ../foo -I ..

If you use ProofGeneral the recommended way is to put file variables to
remember the coqtop options for each file. See pg manual
(http://zermelo.dcs.ed.ac.uk/userman) section "Using file variables".

Regards