aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/OrdersEx.v
Commit message (Expand)AuthorAge
* ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedTypeGravatar letouzey2010-02-09
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07