| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Merge branch 'v8.5' |  Pierre-Marie Pédrot | 2016-01-21 |
| |\ | |||
| | * | Update copyright headers. |  Maxime Dénès | 2016-01-20 |
| * | | CLEANUP: kernel/context.ml{,i} |  Matej Kosik | 2016-01-11 |
| |/ | |||
| * | Fix some typos. |  Guillaume Melquiond | 2015-12-07 |
| * | Removing dead code. | Pierre-Marie Pédrot | 2015-02-02 |
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| * | library/opaqueTables: enable their use in interactive mode |  Enrico Tassi | 2014-10-13 |
| * | Move to a representation of universe polymorphic constants using indices for ... |  Matthieu Sozeau | 2014-08-03 |
| * | - Fix bug preventing apply from unfolding Fixpoints. |  Matthieu Sozeau | 2014-05-06 |
| * | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Lazyconstr -> Opaqueproof | Enrico Tassi | 2014-02-26 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |