The Coq mailing list

[David Pereira <dpereira AT liacc.up.pt>]

Hi Patricia,

Are you  executing the command [Require Import Structures.Orders.] or simply 
[Require Import Orders.] ? If you are doing so, I suspect you have some 
problem with your installation of Coq (or, at least, there is something wrong 
with path where Coq is looking for libraries).

Best regards,
        David.


On Jun 10, 2012, at 4:35 PM, Patricia Peratto wrote:

> The error message is:  Cannot find library Orders in loadpath
> 
> Regards,
> Patricia
> ----- Original Message ----- From: "AUGER Cédric" 
> <sedrikov AT gmail.com>
> To: "Patricia Peratto" 
> <psperatto AT adinet.com.uy>
> Cc: "coqclub" < 
> coq-club AT inria.fr>
> Sent: Sunday, June 10, 2012 6:13 AM
> Subject: Re: [Coq-Club] import
> 
> 
> Le Sat, 9 Jun 2012 18:16:40 -0300,
> "Patricia Peratto" 
> <psperatto AT adinet.com.uy>
>  a écrit :
> 
>> I can not import the file Structures.Orders.
>> Do someone of you know why?
>> Regards
>> Patricia Peratto
> 
> I guess you should provide more informations on your problems if you
> expect an answer. At least, give the error message…