Commit message (Expand) | Author | Age | |
---|---|---|---|
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Follow-up concerning eqb / ltb / leb comparisons | letouzey | 2011-06-21 |
* | Arithemtic: more concerning compare, eqb, leb, ltb | letouzey | 2011-06-20 |
* | A fine-grain control of inlining at functor application via priority levels | letouzey | 2011-01-31 |
* | Numbers and bitwise functions. | letouzey | 2010-12-06 |
* | Numbers: NZPowProp as a Module Type, some module variable renaming | letouzey | 2010-11-02 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType | letouzey | 2010-02-09 |
* | Try to avoid re-declaring Equivalence, especially for Logic.eq | letouzey | 2010-01-13 |
* | Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders* | letouzey | 2010-01-07 |