The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

Here is the response of Jacek Chrzaszcz (it didn't go to the list).

Le 13 mai 04, à 17:10, Jacek Chrzaszcz a écrit :
> This is a known deficiency od the implementation of modules in
> Coq. This is purely a technical problem, but a painful one.
>
> We hope to solve this problem in the future... but it requires heavy
> modifications in many places of the Coq sources....
>
> Jacek


Le 24 mai 04, à 17:37, Frederic Blanqui a écrit :
> i encountered the same problem too. i think that inductives are not 
> seen as
> other definitions. could this be changed in a future version of coq?
>
> --------------- previous message ------------------
> Roland Zumkeller  
> Roland.Zumkeller AT polytechnique.fr
> Thu, 13 May 2004 16:27:09 +0200
>
> I'd like to use modules to do model first-order signatures and algebras
> on them :
>
> Module Type Signature.
>    Variable V : Set.
>    Variable F : nat -> Set.
> End Signature.
>
> When defining the following module
>
> Module S : Signature.
>    Inductive V : Set:= X | Y.
>    Inductive F : nat -> Set:= Plus : F 2 | Zero : F 0 | One : F 0.
> End S.
>
> I get this error message:
>    "User error: Signature components for label V do not match"
>
> However when defining the inductive with another name first, everything
> works fine.
>
> Module S1 : Signature.
>    Inductive V_ : Set:= X | Y.
>    Definition V := V_.
>
>    Inductive F_ : nat -> Set:= Plus : F_ 2 | Zero : F_ 0 | One : F_ 0.
>    Definition F := F_.
> End S1.
>
> Is this a bug or is there a deeper reason for this ?