The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

> I'm working on using Coq extraction but I've run into problems with the
> string type. If I do
>
> Recursive Extraction Library String.
>
> I get the coq string library, but the name String conflicts with the
> ocaml String library so when I link my code it can't resolve references.

I don't know of any really clean solution to this problem, but see an
earlier message of mine for two possible approaches:

http://pauillac.inria.fr/pipermail/coq-club/2007/003005.html

Hope this helps,

- Xavier Leroy