Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Better handling of the universe context in case of Admitted proof obligations. | 2014-07-10 | |
* | Proofs now take and return an evar_universe_context, simplifying interfaces | 2014-06-18 | |
* | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of | 2014-06-08 | |
* | - Fix in kernel conversion not folding the universe constraints | 2014-05-26 | |
* | This commit adds full universe polymorphism and fast projections to Coq. | 2014-05-06 | |
* | Adding a stm/ folder, as asked during last workgroup. It was essentially moving | 2014-04-25 |