The Coq mailing list

["Jay McCarthy" <jay.mccarthy AT gmail.com>]

This may be an OCaml problem, but I imagine it has been discovered
first with Coq.

I have extracted a program that uses Coq.Lists.List. I am linking this
against an OCaml program that uses the OCaml stdlib (actually not even
using stdlib's List, although I want to); I get the following error:

ocamlopt \
                          \
                                        -o wpplc \
                        datatypes.cmx specif.cmx orderedType.cmx
setoid.cmx peano.cmx binPos.cmx binNat.cmx binInt.cmx compare_dec.cmx
orderedTypeEx.cmx bool.cmx list.cmx fSetInterface.cmx fSetFacts.cmx
fSetProperties.cmx fSetList.cmx fMapList.cmx dOrderedType.cmx
constants.cmx common.cmx cPPL.cmx wPPL.cmx wPPLi.cmx pos.cmx
ast_ut.cmx parser.cmx scanner.cmx
Files list.cmx
and /Users/jay/Development/dists/ocaml/godi/lib/ocaml/std-lib/stdlib.cmxa
both define a module named List

I can think of two solutions:

1) Get program extraction to rename list.ml to something else, such as
coq_list. (Basically, perform the name mangling it already does with
constants like nil, but on filenames that match the standard library)

2) Get OCaml to accept this situation and allow two modules with one
name, perhaps by internal name mangling

Does anyone know the appropriate magic to get this to work?

Jay

-- 
Jay McCarthy 
<jay.mccarthy AT gmail.com>
http://jay.teammccarthy.org