aboutsummaryrefslogtreecommitdiff
path: root/theories/Structures/OrdersTac.v
AgeCommit message (Expand)Author
2010-01-17BigN, BigZ, BigQ: presentation via unique module with both ops and propsletouzey
2010-01-17Simplification of OrdersTac thanks to the functor application ! with no inlineletouzey
2010-01-13Try to avoid re-declaring Equivalence, especially for Logic.eqletouzey
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey