coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Simple question about libraries

From: Adam Chlipala <adam AT chlipala.net>
To: Edsko de Vries <edskodevries AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Simple question about libraries
Date: Sun, 20 Jun 2010 10:11:50 -0400

Edsko de Vries wrote:

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?

You'll find an explanation at the end of Chapter 14 of CPDT:
http://adam.chlipala.net/cpdt/
http://adam.chlipala.net/cpdt/html/Large.html

[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