The Coq mailing list

["Marko Maliković" <marko AT ffri.hr>]

Did you type:

Require Import Structures.Orders.

In Coq 8.3pl3 it works OK for me.

Marko Malikovic

> 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…
>


-----------------------
Dr. Sc. Marko Maliković
Docent
Filozofski fakultet
Sveučilište u Rijeci
---------------------
Ph.D. Marko Maliković
Assistant Professor
Faculty of Humanities and Social Sciences
University of Rijeka, Croatia
-----------------------------
marko.malikovic AT ffri.hr
http://www.ffri.hr/~marko
-------------------------