The Coq mailing list

[Jelle <jelle AT defekt.nl>]

Hello,

When running Coq with "-impredicative-set" I would have expected the
following to work:

 Record foo : Set := mkFoo { bar : Set }.
 foo is defined
 foo_ind is defined
 foo_rec is defined

But the projection is not defined:

 Warning: bar cannot be defined because it is large and foo is not.

Trying this manually gives:

 Definition bar (x : foo) := match x with mkFoo b => b end.

 Error: Incorrect elimination of "x" in the inductive type "foo":
 the return type has sort "Type" while it should be "Prop" or "Set".

 Elimination of an inductive object of sort Set is not allowed on a
 predicate in sort Type because strong elimination on non-small
 inductive types leads to paradoxes.

What is going on here? -impredicative-set doesn't work with records?
And what exactly is strong elimination?

Thanks for clarifying,

Jelle.