The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  Hi Christian,

  Try:

Module Type S.

 Parameter X : Type.

End S.

Module False : S.

 Inductive XX := .

 Definition X := XX.

End False.

  That's what the hint was trying to tell you, I think.

  Cheers,

  Adam

On Wed, Dec 9, 2009 at 16:36, Christian Doczkal <doczkal AT ps.uni-sb.de> wrote:

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

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [15 rue Berlier, 75013 Paris, France]