The Coq mailing list

[Frederic Blanqui <blanqui AT loria.fr>]

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 ?