Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau | 2014-06-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | 2014-03-05 |
* | Support for evars and metas in native compiler. | Maxime Dénès | 2013-12-30 |
* | More monomorphization. | ppedrot | 2013-03-05 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |