Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Update headers following #6543. | 2018-02-27 | |
* | This commit adds full universe polymorphism and fast projections to Coq. | 2014-05-06 | |
* | Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904) | 2012-12-18 | |
* | Reverted 13293 commited mistakenly. Sorry for the noise. | 2010-07-18 | |
* | Tentative de suppression de l'import automatique des hints et coercions. | 2010-07-18 | |
* | BigN, BigZ, BigQ: presentation via unique module with both ops and props | 2010-01-17 | |
* | Simplification of OrdersTac thanks to the functor application ! with no inline | 2010-01-17 | |
* | Try to avoid re-declaring Equivalence, especially for Logic.eq | 2010-01-13 | |
* | Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders* | 2010-01-07 |