The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Le mercredi 06 juillet 2005 à 12:57 +0200, 
anoun AT labri.fr
 a écrit :
> Hi all,
> I have an application in Coq which is composed of several directories, I 
> want to
> know how we can load all the paths of the different directories so that we 
> will
> be able to export easily different files...
> For instance, if we assume that we have two directories der1 der2, where 
> der1
> contains file1 and file2 and dir2 contains file3 which needs to export 
> file1...

> Should we add in the beginning of all files the command 'Add LoadPath 
> ".."?? Or
> is there a more elegant solution with the interface coqide?

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

Regards,

Guillaume