coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] FMap on Int

From: Ashish Darbari <ashish_darbariuk AT yahoo.co.uk>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] FMap on Int
Date: Tue, 20 Jan 2009 12:48:55 +0000 (GMT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.co.uk; h=X-YMail-OSG:Received:X-Mailer:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type:Message-ID; b=KGkbPsE+Y0TkxLmgHd6O+vH/LE09gzUbEBTYoPz8FXx7D+18KETN179ac84reNeDlu8zN16oQSOB5ltTDcFehKrw7mv4PKVdfzbB6qUSqQPStg0zUivFK/dxx71gjQ6Gw4A1m2M1abdpP7VOpSfHvszOcA8JT3e/6J60d5Tlal4=;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I'm having problems able to use the FMapAVL.
It works out quite fine if I want the keys 
to have the type z (IMap), but since I want to use
this map in ocaml extracted code where keys
will be ocaml integers, I want to define the
equivalent module (IMap1) in Coq on Ints, but
when I do it as shown below, I get an error,
No such label lt. 

What am I missing?

Thanks
Ashish

Require Import ZArith.
Require Import OrderedType.
Require Import OrderedTypeEx.
Require Import FMapAVL.
Require Import Int.


Module IMap :=
 FMapAVL.Make(Z_as_OT).

Module IMap1 := FMapAVL.Make(Z_as_Int).

[Coq-Club] FMap on Int, Ashish Darbari
- Re: [Coq-Club] FMap on Int, Filou Vincent
- Re: [Coq-Club] FMap on Int, Pierre Letouzey
  - Re: [Coq-Club] FMap on Int, Ashish Darbari