coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Simple question about libraries

From: Edsko de Vries <edskodevries AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Simple question about libraries
Date: Sun, 20 Jun 2010 14:50:29 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=EWc/Qozw1PXGAHW5RcAeDBgY5bg9KOk+UkkbSWC0M3fHQP94jMcb+xgv7mHauAw2Jk +ZS1OTc/MU8Ix8scZeFPhhEH3IKPX0oBDi5zcwKBGoYDu+GhtKpM1rGzDSVkysrqqR+n PBmADV9g/jGRJIDucvGtZwdn8NZtSPYRXvSko=

Hi,

Simple question. Suppose I have a file Foo.v in a directory A, and I
want to load this file using

Require Import A.Foo

in a script B/Bar.v. If I do

coqc A/Foo.v
coqc B/Bar.v

then I get

File ".../B/Bar.v", line 1, characters 0-21:
Error: The file .../A/Foo.vo contains library Foo and not library A.Foo

What's the correct way to do this?

Thanks,

Edsko

[Coq-Club] Simple question about libraries, Edsko de Vries
- Re: [Coq-Club] Simple question about libraries, Adam Chlipala
- Re: [Coq-Club] Simple question about libraries, Roman Beslik
  - Re: [Coq-Club] Simple question about libraries, Edsko de Vries
    - Re: [Coq-Club] Simple question about libraries, Hugo Herbelin