The Coq mailing list

[Ali Assaf <ali.assaf AT inria.fr>]

Hello,

I have a problem with Coq not finding ML modules in the loadpath. Suppose I have a folder [foo] with an ML module [bar.cmxs] and a Coq library [baz.vo]. If I lauch Coq with [-R foo Foo] then change the current directory with [Cd ".."], I can load the Coq library with [Require baz] with no problem. However when I try to load the ML module with [Declare ML Module "bar"] I get the following error:

Error: File not found on loadpath : bar.cmxs

What am I missing? Note that this problem does not appear if I don't change the current directory with [Cd ".."].

Thanks,

Ali Assaf