| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | 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 |
| * | Opaqueproofs: sink futures when interactive | Enrico Tassi | 2014-04-25 |
| * | Lazyconstr -> Opaqueproof | Enrico Tassi | 2014-02-26 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |