The Coq mailing list

[Wojciech Moczydlowski <wm174746 AT zodiac.mimuw.edu.pl>]

  Hello,

I'm a Ph. D. student in computer science and a newbie to Coq. During my 
sessions with it I encountered the following behavior:

If I declare

Variable x : Type -> Type 

in Coq 8.0

then (x nat) typechecks, that is Check (x nat) says that (x nat) : Type. 
This seems weird, for I do not see how to derive nat : Type from the 
inference rules in the documentation on the webpage, which seem to be 
necessary to derive (x nat) : Type. What am I missing?

Thanks.

Wojtek