The Coq mailing list

[Jacek Chrzaszcz <chrzaszc AT mimuw.edu.pl>]

On Thu, Jan 15, 2004 at 06:08:45PM +0200, Jevgenijs Sallinens wrote:
> Dear Pierre,
> 
> I suspect there is some fundamental difference with the case when inductive
> types and fixponts are not used in module types. In the latter case I havn't
> found similar problems.
> 
> Writing like NA2.NA. is a bit ugly, but what is worth, this could became
> unmanageble when there are many related modules.
> In the example below, I have added yet another module I_Nat3 without its
> implementation.
> Now in Nat_Test one result should be taken from I_Nat2 and another from
> I_Nat3. I suspect, now it is impossuble to finish the proof of Nat_Test
> without introducing new module where both I_Nat2 and I_Nat3 are
> imported. (NA3.NA and NA2.NA are conflicting)
> 
> Yet another problem, I have discovered after sent original mail, is that
> lemma Nat_2 not recognized as having the same type as Axiom Nat_2
> in the module type I_Nat2,  if  verification like
> Module Nat2[NA:I_Nat]:I_Nat2 with Module NA:=NA.
> is imposed.
> 

Dear Jevgenijs,

The script included in your mail works both in V8beta and V7-4-bugfix CVS
branch. In V7.4 there were indeed some problems related to names of
inductive types which were normal forms in V7.3 but not any more when
modules have been introduced. Of course errors in some tactics have been
found and corrected only after people like you started using modules. Thanks!

> If these problems are real, I think the usage of inductive definitions
> in module types are not reliable for large projects.

Please do and tell us where the bugs are!

Jacek