The Coq mailing list

[Ashish Darbari <ashish_darbariuk AT yahoo.co.uk>]

Thank you, Stephen and Adam. I can download

the svn snapshot and check the Blacklist

option, but clearly there must be more 

people out there who may have used Finite

Maps in their work, I would like to see

some examples and some thoughts from 

people on efficiency issues, I mean did

people find it too slow to use the extracted

code or reasonable. Where is the best place

to get this info? 

Thanks

Ashish

---

From: St�phane Lescuyer <lescuyer AT lri.fr>
To: Adam Chlipala <adamc AT hcoop.net>
Cc: Ashish Darbari <ashish AT darbari.org>; coq-club AT pauillac.inria.fr
Sent: Sunday, 11 January, 2009 19:22:28
Subject: Re: [Coq-Club] Finite Maps

There was indeed a discussion about this issue earlier in December and
Pierre Letouzey pointed to a new command

Extraction Blacklist <module name> .... .

that forces the extraction mechanism to rename modules like List and
String, in order to avoid clashes with the usual OCaml modules.
That would solve your issue without resorting to -pack (or worse, to sed).
It is only available in the svn snapshot or the current 8.2 beta version though.

HTH,

Stéphane L.


On Sun, Jan 11, 2009 at 8:12 PM, Adam Chlipala <adamc AT hcoop.net> wrote:
> Ashish Darbari wrote:
>>
>> However having compiled these using ocaml compilers and loading (#use)
>>
>> the fMapAVL.ml I get an error message
>>
>> The file ocaml and fMapList.cmi make inconsistent assumptions over
>> interface List
>>
>
> I expect that you extracted a file list.ml, which conflicts with [List] from
> the OCaml standard library.  Check out the [-pack] option to the OCaml
> compilers for a way to put your extracted modules in a separate namespace
> and avoid the clash.
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>        http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06