Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Reverted 13293 commited mistakenly. Sorry for the noise. | herbelin | 2010-07-18 |
* | Tentative de suppression de l'import automatique des hints et coercions. | herbelin | 2010-07-18 |
* | BigN, BigZ, BigQ: presentation via unique module with both ops and props | letouzey | 2010-01-17 |
* | Simplification of OrdersTac thanks to the functor application ! with no inline | letouzey | 2010-01-17 |
* | Try to avoid re-declaring Equivalence, especially for Logic.eq | letouzey | 2010-01-13 |
* | Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders* | letouzey | 2010-01-07 |