The Coq mailing list

[vincent.chatel AT transport.alstom.com]

Hi,

I'm using the following construction  :

Require Arith.
Set Implicit Arguments.

Inductive listn : nat->Type :=
  niln:(listn O)
 | consn :(A:Type)(n:nat) A->(listn n)->(listn (S n)).

When I try to build listn with elements of type listn :

Parameter X:Type.
Parameter x1,x2:X.

Definition l1 := (consn x1 (consn x2 niln)).  (* OK *)
Definition l2 := (consn l1 niln)

Coq answers "Error: Universe Inconsistency"

But if I change "Type" by "Set" :
Inductive listn : nat->Set :=
  niln:(listn O)
 | consn :(A:Set)(n:nat) A->(listn n)->(listn (S n)).

l2 is defined.

Why I cannot build listn of listn with "Type".