The Coq mailing list

[Kevin Sullivan <sullivan.kevinj AT gmail.com>]

Intuitively this should not work. And it doesn't.

    Inductive E: Set := .

    Definition p: Prop := E.

But this does.

    Inductive P: Prop := .

    Definition s: Set := P.

Can someone point me to the right part of the manual to determine how best to explain why?

KS