Hi,

I’m working on developing a compiler in Coq, and I need to use sets & maps. So far I’ve been using FSetAVL and FMapAVL, which let me compute examples in Coq and extract nicely to OCaml. But I’d really just like to use OCaml’s sets and maps. I realize this defeats the purpose of having verified set/map implementations, but I’d like the extracted code to be as concise as possible, and when I tried manually editing the extracted code to use OCaml’s sets and maps it improved performance significantly.

For reference, I’m using FSetAVL and FMapAVL in this file.

I thought something like the following might work:

```
Module FSet := FSetAVL.Make(Coq.Structures.OrderedTypeEx.Nat_as_OT).
Extract Constant FSet.union => "...".
Recursive Extraction FSet.union.
```

But this doesn’t seem to do anything. It just extracts the normal AVL implementation.

I could axiomatize maps/sets and use “Extract Constant” on my axiomatization, but I don’t want break my existing proofs and I like being able to compute examples within Coq.

Any tips?

Thanks.