The Coq mailing list

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

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 ?