| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs. |  Arnaud Spiwack | 2014-10-22 |
| * | Better handling of the universe context in case of Admitted proof obligations. |  Matthieu Sozeau | 2014-07-10 |
| * | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
| * | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of |  Pierre-Marie Pédrot | 2014-06-08 |
| * | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | 2014-05-26 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Adding a stm/ folder, as asked during last workgroup. It was essentially moving | Pierre-Marie Pédrot | 2014-04-25 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |