The Coq mailing list

[Michel Levy <michel.levy1948 AT gmail.com>]

I'm using  Coq 8.4pl3 (January 2014) with coqtop.
I try this (classical) example :
Coq<Definition id (T:Type)(x:T):=x.
Coq<Check (id (forall T:Type,T->T) id)
I was expecting an error, because the id declared is typed forall T: Type(i),T->T
while it is expected to be typed forall T:type(j),T->T where i and j are any naturals numbers.

But with this Coq version, I have
Coq < Check (id (forall T:Type,T->T) id).
id (forall T : Type, T -> T) (fun T : Type => id T)
     : forall T : Type, T -> T

I don't understand why the left id is replaced by (fun T:Type => id T), especially because id and (fun T:Type => id T) have
the same type.

-- 
email : michel.levy1948 AT gmail.com
http://membres-liglab.imag.fr/michel.levy