The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Le 10/03/2016 17:33, Ralf Jung a écrit :
> So I wonder, would it be possible to add a flag to Coq to disable the
> elim restriction? Would that make sense? It's a little like
> type-in-type, except that it's not actually unsound if not combined with
> classical axioms.

If I remember correctly, this restriction is important to soundness :
because Prop is impredicative, we can build a proof of false from
inhabited T -> T.

-- JH

Attachment: signature.asc
Description: OpenPGP digital signature