The Coq mailing list

[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: 

- First, there is currently no way of retreiving the "with" constructs
written by the user at the Coq level and reuse them when extracting
signatures. These "with" are in fact syntactic sugar that is expanded
during the Coq processing. It's then close to impossible for the
extraction to guess back these "with" at the other end of the
processing. It's a pity, I agree, and I would love to see these "with"
becoming first-class constructions in Coq. But I've no time for doing
it myself. Moreover, someone is working currently on a reform of these
modules and I don't fully understand yet if a primitive "with" would
fit in the new approach.

- Now, concerning the bug itself, I've found the Coq structure that 
make things work at the Coq level: it's a field mind_equiv that allow
a inductive to be aliased in another module. I'm currently working 
on replicating this field at the extraction level. Most of the work is
done I think, but at the end I need to be able to print something like 
  let t = M.t = Foo | Bar
And this printing involves some name resolution that is failing for
the moment. Work in progress, I will let you know when I've finished
the debugging. 

Sorry once more for the delay

Pierre Letouzey