The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Try passing `-R . Somename` to coqc/coqtop/coq_makefile, and then using Somename.MyMod.

-Jason

On Jan 7, 2015 5:16 PM, "Peter LeFanu Lumsdaine" <p.l.lumsdaine AT gmail.com> wrote:

On Wed, Jan 7, 2015 at 3:08 AM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

I think the "Top." prefix always works for anchoring absolute names: Top.MyMod

That does not seem to work: [Require Import Top.MyMod] gives

> Error: Cannot find library Top.MyMod in loadpath

while, for comparison, [Require Import MyMod] gives

> Warning: MyMod.vo has been found in

>  [ /Users/peterlefanulumsdaine/[…]/mydir/D2 ;

>    /Users/peterlefanulumsdaine/[…]/mydir/D1 ;

>    /Users/peterlefanulumsdaine/[…]/mydir ];

>  loading /Users/peterlefanulumsdaine/[…]/mydir/D2/MyMod.vo

If I am understanding the manual correctly, Top is the module in which objects defined during the current session are placed, so "Top.foo" is the absolute name of a newly defined object "foo"; but imported libraries are not within Top.

–p.