aboutsummaryrefslogtreecommitdiff
path: root/theories/Structures/OrderedType.v
AgeCommit message (Expand)Author
2010-01-17Simplification of OrdersTac thanks to the functor application ! with no inlineletouzey
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey
2010-01-07Include can accept both Module and Module Typeletouzey
2010-01-07OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...letouzey
2009-11-03OrderedType implementation for various numerical datatypes + min/max structuresletouzey
2009-10-19Merge SetoidList2 into SetoidList.letouzey
2009-10-16Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...letouzey
2009-10-14Improved tactic "order" in OrderedTypeletouzey
2009-10-13MSets: a new generation of FSetsletouzey