aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelambda.ml
Commit message (Expand)AuthorAge
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Avoid warnings about loop indices.Gravatar Guillaume Melquiond2016-01-02
|/
* Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Fixing some English misspelling.Gravatar Hugo Herbelin2015-07-29
* Fix vm compiler to refuse to compile code making use of inductives withGravatar Matthieu Sozeau2015-03-25
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fix exponential behavior in native compiler with retroknowledge.Gravatar Maxime Dénès2014-04-09
* Optimizing Int31 support in native compiler, by not taggingGravatar Maxime Dénès2014-04-09
* Int31 decompilation in native compiler was still partial. Now fixed.Gravatar Maxime Dénès2014-04-09
* Machine arithmetic operations for native compiler.Gravatar Maxime Dénès2014-04-09
* Full support for int31 values in native compiler.Gravatar Maxime Dénès2014-04-09
* Partial support for open terms in int31.Gravatar Maxime Dénès2014-04-09
* Had to split Nativelambda in two files because of RetroknowledgeGravatar Maxime Dénès2014-04-09
* Int31 literals in native compiler.Gravatar Maxime Dénès2014-04-09
* Fixing generic hashes and replacing them with proper ones.Gravatar Pierre-Marie Pédrot2014-03-03
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
* Got rid of unused lazy flag in the native compiler.Gravatar Maxime Dénès2013-12-29
* Removing native_name reference from constant_body.Gravatar Maxime Dénès2013-12-28
* Fixing a bug in the native compiler, introduced by r16363, leading to undefinedGravatar mdenes2013-07-06
* Native compiler: hash-consing of generated code and values.Gravatar mdenes2013-03-25
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
* More monomorphization.Gravatar ppedrot2013-03-05
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Fixing bug in native compiler with let patterns in fixpoint definitions.Gravatar mdenes2013-02-11
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22