| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Update headers following #6543. |  Théo Zimmermann | 2018-02-27 |
| * | 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 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |