| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | This commit adds full universe polymorphism and fast projections to Coq. |  Matthieu Sozeau | 2014-05-06 |
| * | Readback for int31 values from native compiler. |  Maxime Dénès | 2014-04-09 |
| * | 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 |
| * | Splitting Term into five unrelated interfaces: |  ppedrot | 2013-04-29 |
| * | Native compiler: timing info for reification in debug mode. |  mdenes | 2013-03-25 |
| * | Restrict (try...with...) to avoid catching critical exn (part 12) |  letouzey | 2013-03-13 |
| * | Term.dest* functions now raise specific DestKO exn instead of Invalid_argument | letouzey | 2013-03-12 |
| * | More monomorphization. | ppedrot | 2013-03-05 |
| * | More informative error when a global reference is used in a context of |  herbelin | 2013-02-28 |
| * | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
| * | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |