aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/OrdersTac.v
Commit message (Expand)AuthorAge
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* BigN, BigZ, BigQ: presentation via unique module with both ops and propsGravatar letouzey2010-01-17
* Simplification of OrdersTac thanks to the functor application ! with no inlineGravatar letouzey2010-01-17
* Try to avoid re-declaring Equivalence, especially for Logic.eqGravatar letouzey2010-01-13
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07