| 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 |
| * | Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904) |  letouzey | 2012-12-18 |
| * | 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 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |