aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/OrdersEx.v
Commit message (Expand)AuthorAge
* MMapPositive: another implementation of MMapsGravatar Pierre Letouzey2015-03-06
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* Modularization of BinNat + fixes of stdlibGravatar letouzey2011-05-05
* Integer division: quot and rem (trunc convention) in addition to div and modGravatar letouzey2010-11-10
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* NPeano improved, subsumes NatOrderedTypeGravatar letouzey2010-02-09
* NBinary improved, contains more, subsumes NOrderedTypeGravatar letouzey2010-02-09
* ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedTypeGravatar letouzey2010-02-09
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07