Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Update headers. | Maxime Dénès | 2015-01-12 |
* | Fix for #3154: use CUnix.sys_command to call native compiler. | Maxime Dénès | 2014-12-16 |
* | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin | 2014-09-13 |
* | 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 |