coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] module problem

From: Marc Bezem <Marc.Bezem AT ii.uib.no>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] module problem
Date: Thu, 20 Jan 2005 16:09:23 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

why do I get:

Coq < Require Arith.
Error: The file /usr/lib/coq/theories/Arith/Arith.vo contains library
Coq.Arith.Arith and not library Arith.Arith

Coq < Require Setoid.
Error: The file /usr/lib/coq/theories/Setoids/Setoid.vo contains library
Coq.Setoids.Setoid and not library Setoids.Setoid

and so ? (I'm still running Coq 7.4)

Many thanks,

Marc

[Coq-Club] module problem, Marc Bezem