| Age | Commit message (Expand) | Author |
|---|
| 2016-02-09 | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-11 | CLEANUP: kernel/context.ml{,i} | Matej Kosik |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond |
| 2015-07-29 | Fixing some English misspelling. | Hugo Herbelin |
| 2015-07-10 | Native compiler: refactor code handling pre-computed values. | Maxime Dénès |
| 2015-06-08 | Fix native compilation of primitive projections. Closes #4210. | Maxime Dénès |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot |
| 2015-01-17 | Make native compiler handle universe polymorphic definitions. | Maxime Dénès |
| 2015-01-15 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-11-12 | Cleaner interfaces for linking locations of native compiler. | Maxime Dénès |
| 2014-10-24 | No hash consing across calls to the native compiler. | Maxime Dénès |
| 2014-10-20 | A patch for printing "match" when constructors are defined with let-in | Hugo Herbelin |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-05-01 | Fixing ml-doc. | Pierre-Marie Pédrot |
| 2014-04-09 | Fix exponential behavior in native compiler with retroknowledge. | Maxime Dénès |
| 2014-04-09 | Optimizing Int31 support in native compiler, by not tagging | Maxime Dénès |
| 2014-04-09 | Machine arithmetic operations for native compiler. | Maxime Dénès |
| 2014-04-09 | Full support for int31 values in native compiler. | Maxime Dénès |
| 2014-04-09 | Partial support for open terms in int31. | Maxime Dénès |
| 2014-04-09 | Had to split Nativelambda in two files because of Retroknowledge | Maxime Dénès |
| 2014-04-09 | Int31 literals in native compiler. | Maxime Dénès |
| 2014-03-03 | Fixing generic hashes and replacing them with proper ones. | Pierre-Marie Pédrot |
| 2014-03-01 | Hunting pervasive equality in native compiler. It seems they were used for | Pierre-Marie Pédrot |
| 2014-02-26 | Lazyconstr -> Opaqueproof | Enrico Tassi |
| 2013-12-30 | Support for evars and metas in native compiler. | Maxime Dénès |
| 2013-12-29 | Got rid of unused lazy flag in the native compiler. | Maxime Dénès |
| 2013-12-28 | Removing native_name reference from constant_body. | Maxime Dénès |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-24 | Specializing hash functions for widely used types. | ppedrot |
| 2013-10-24 | Turn many List.assoc into List.assoc_f | letouzey |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-07-06 | Fixing a bug in the native compiler, introduced by r16363, leading to undefined | mdenes |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-25 | Native compiler: hash-consing of generated code and values. | mdenes |
| 2013-03-25 | Native compiler: Inlined constants are now compiled, fixing a bug reported by | mdenes |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 8) | letouzey |
| 2013-03-12 | invalid_arg instead of raise (Invalid_argement ...) | letouzey |
| 2013-03-05 | More monomorphization. | ppedrot |
| 2013-02-26 | kernel/declarations becomes a pure mli | letouzey |
| 2013-02-26 | Names: shortcuts for building {kn, constant, mind} with empty sections | letouzey |
| 2013-02-18 | use List.rev_map whenever possible | letouzey |
| 2013-02-11 | Fixing bug in native compiler with let patterns in fixpoint definitions. | mdenes |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-28 | native_compute: Fixed dependencies compilation order. | mdenes |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
