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