The Coq mailing list

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

In my application I need to use an IntMap essentially a table of key-bindings 

where keys are always (positive) integers, currently  in ocaml I use the following 

module myMap = Map.Make

(struct type t = int

let compare = compare end);;

This exposes me to the full API for the IntMaps and I can 

use add, delete, find etc for it.  I wanted to be able to get 

a similar if not exactly the same functionality from extraction in Coq. I'd

a look at the FMapAVL library and from the documentation it

appears that executing it in extracted world is reasonably fast.

(well as best as one gets from a Balanced Binary Tree) 

I wanted to test the extracted ocaml code, so I did the following

to extract it in Coq 8.1pl4 :

Coq > Require Import FMapAVL.

Coq > Recursive Extraction Library FMapAVL.

and I get the following blurb:

The file logic.ml has been created by extraction.

The file logic.mli has been created by extraction.

The file datatypes.ml has been created by extraction.

.

.

.

The file fMapAVL.ml has been created by extraction.

The file fMapAVL.mli has been created by extraction.

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

How to fix this? 

Is there an example somewhere I can see on how FMapAVL has been used

in practice for extraction? Can someone point me to any efficiency results for

the extracted FMaps in ocaml?

Thank you

Ashish