The Coq mailing list

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

  Hello,

I guess my previous question regarding impredicativity of Prop in Coq was 
too vague to be answered. I'll try to reformulate it:

Does anyone know about any developments in Coq's standard library which 
would stop "working" if impredicativity from Prop was removed in the same 
way the impredicativity of Set was removed in transition to version 8.0? 
That is, if the first Prod rule in the reference manual, instead of being 
generated by tuples (Type, Prop, Prop), (Set, Prop, Prop), (Prop, Prop, 
Prop), 
would be generated only by (Set, Prop, Prop) and (Prop, Prop, Prop). 

If not, does someone have a suggestion how to find out? Looking through 
the standard library by hand doesn't seem to be the right approach (though 
maybe I'm missing something very obvious and the answer is trivial). 
I was thinking about taking Coq's sources, removing the respective 
typing rule and trying to somehow "recompile" the standard library, 
but I'm not sure if this has a chance of succeeding. 

Thanks, 

Wojtek