The Coq mailing list

["St�phane Lescuyer" <lescuyer AT lri.fr>]

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