The Coq mailing list

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

Quoting Pierre Letouzey 
<Pierre.Letouzey AT pps.jussieu.fr>:

> On Mon, Dec 04, 2006 at 02:46:25PM +0000, Robert Atkey wrote:
> > 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?
>
> Sorry for not having answered yet your first bug report. I was
> planning to fix the issue and then give an answer, but this plan has
> been overly delayed. So here's today's status of this bug:

Pierre,

Thanks for the update and all your work on this. As I said, a solution 
to this bug would be very useful to me, so I really appreciate the work 
you are doing.

Bob Atkey