The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-sb.de>]

I just stumbled across the following: 

Module Type S.
  Parameter X : Type.
End S.

Module False : S.
  Inductive X := .
End False.

(* Error: The kernel does not recognize yet that a parameter can be
instantiated by an inductive type. Hint: you can rename the inductive
type and give a definition to map the old name to the new name. *)

(* Of course one can circumvent the problem like this, but it removes a
lot of the structuring effect one would like Modules to have ...

Inductive FalseT : Type := .

Module FT : S.
  Definition X := FalseT.
  Definition R := @eq FalseT.
End FT.

Is there any work being done on the subject?
Are there any theoretical issues?

-- 
Regards
Christian Doczkal