The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> 1) i wanted to add some folders to the LoadPath. i tried under coqtop,
> and i can see them  with "Print LoadPath.", but still my Require
> Import does not work. I read in the archives of this mailing list,
> that the Add Loadpath ... works also from inside the coqide, which it
> does for me, but still it is a dirty workaround to include Add
> LoadPath ... in all files.
> Is this a known problem or does anybody know how to fix it?
> (i think my Add LoadPath was correct, as it works in coqIde)

It is in general better to call coqtop with option "-I dir" or "-R dir
mywork" where dir is the name of your directory and mywork a "logical"
name used to refer to your work from the Coq side. Then, the contents
of your files get independent of where there lives in the file system.
For further details, see:

 
http://coq.inria.fr/distrib/v8.2/refman/Reference-Manual017.html#@default777

This is easy to do from a terminal under Unix (and in particular under
MacOS X). If your environment is Windows, you should ask a specialist.

Alternatively, you can also add "Add LoadPath" commands in some .coqrc
file in your home directory. For details, see

 
http://coq.inria.fr/distrib/v8.2/refman/Reference-Manual017.html#@default781

> 2) i have a Local Open Scope command that works in three files, but
> not in the third. the "Required Import ..."s are the same (so the
> scope should be accessible). the only difference, that i could find
> and thought it could be important, is that i have the .vo-files for
> the two files where it works (i had them before i opened and tried the
> .v files as it there was an install and compile routine), and for the
> one where it does not work i don't have it. any ideas where i should
> start searching for a solution?

This is difficult to say without the precise example. You can use the
commands "Print Visibility" and "Print Scopes" to try to diagnose the
problem.

Best regards,

Hugo Herbelin