The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

On Fri, Dec 30, 2011 at 1:36 PM, Stéphane Glondu <steph AT glondu.net> wrote:

You have to issue "#directory" directives first:

 #directory "/usr/lib/coq/interp";;
 #directory "/usr/lib/coq/kernel";;
 #directory "/usr/lib/coq/lib";;
 #directory "/usr/lib/coq/library";;
 etc.

one for each directory containing the .cmi file of a module you want to
access (adapt /usr/lib/coq/ accordingly). With zsh, you can generate a
"directories" file with the following command:

for u in $COQROOT/**/*.cmi; do echo '#directory "'"${u%/*}"'";;'; done |
sort -u > directories

Then, you can run '#use "directories";;' before running commands from
e.g. dev/include.

It seems that #directory are implicit for each "-I" given when linking
coqtop.byte, which may explain why you don't have to run them when the
source tree is still there.


Cheers,

--
Stéphane

Thanks Stephane for your detailed answer, and also thanks to Hugo, Jeremie, and Andrej for helping me figure out what was going on.

Happy new year,
Beta