| 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 |
| |/ | |||
| * | Avoid type checking private_constants (side_eff) again during Qed (#4357). |  Enrico Tassi | 2015-10-28 |
| * | 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 |