The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> CHAUVIN Barnabe 
>>>>> <barnabe.chauvin AT gmail.com>
>>>>>  writes:

> In Rdefinitions, I found the is_upper_bound definition, which represent the
> R set with the type R->Prop. It would be more understandable if it would be
> "Ensemble R", isn't it ? (This is the reason why I said I feel like the
> theories are not working together ..)

I've also found a few places where it seems that some parts of the stdlib
evolved separately from other parts, and at different times, so that they
express similar things in ways that are different enough to be cumbersome.

It might be nice to overhaul and create a stdlib v2, based on all the
experience gained thus far, using the most modern features of the upcoming Coq
8.5, and aiming at better consistency to a whatever core philosophy is chosen.

This is one reason why I've settled on ssreflect, and moved away from using
the stdlib, because they've definitely got the consistency going there.

John