The Coq mailing list

[Nils J�hnig <jaehnig AT mi.fu-berlin.de>]

Hi,

i am new to coq and have two problems.

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)

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?

i have the version 8.2pl1

please tell me, if there is information missing.

Best regards
Nils