The Coq mailing list

[Robert Atkey <bob.atkey AT ed.ac.uk>]

Hello,

Has there been any progress on Bug #1239 (which I reported), which is
about the extraction of shared inductive types in module signatures
being incorrect?

This bug is currently impeding the work I want to do with Coq. I have a
large development containing extractable code as a functor abstracted
over the implementation of some basic data types that I want to
implement in O'Caml. My previous design had a large tower of functors
that built on the previous one. This design took about 1.5-2hrs to
extract!

My new design, using a flatter arrangement of functors, works much
better -- it extracts in under 5 minutes! -- however Bug #1239 prevents
the extracted code from being usable.

I have tested the test case in the bug report on the SVN version of Coq
and the bug is still present.

Thanks,
Bob Atkey