The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

I encountered the following behavior, which I find strange....

Inductive b : Type := t1 | t2.
Inductive I : list Type -> Type -> Type :=
| C : I (b :: b :: nil) unit.

The term "I" of type "list Type -> Type -> Type"
cannot be applied to the terms
 "b :: b :: nil" : "list Set"
 "b" : "Set"
The 1st term has type "list Set" which should be coercible to "list Type".

Could someone explain me what's happening ? NB: I tried to redefine
list by myself, making sure that everything is in Type, but it does
not work either.

Cheers,
Thomas