aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/NatOrderedType.v
Commit message (Expand)AuthorAge
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03