The Coq mailing list

[Loic Pottier <loic.pottier AT inria.fr>]

Hello,

with coq-8.3:

Inductive paths (T:Type)(t:T): T -> Type :=   idpath: paths _ t t.

Check (forall X:Type, paths _ X X).

returns

forall X : Type, paths Type X X

     : Prop

But I expected Type instead of Prop... where from does this Prop come???

Loïc