aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelambda.ml
Commit message (Expand)AuthorAge
* [env.env_rel_context.env_rel_ctx] -> [rel_context env]Gravatar Gaëtan Gilbert2018-06-28
* Merge PR #7772: [native_compute] Delay computations with toplevel matchGravatar Pierre-Marie Pédrot2018-06-24
|\
* | Change the proj_ind field from MutInd.t to inductive.Gravatar Pierre-Marie Pédrot2018-06-23
| * [native_compute] Delay computations with toplevel matchGravatar Maxime Dénès2018-06-11
|/
* Use projection indices in native compilation rather than constant names.Gravatar Pierre-Marie Pédrot2018-06-05
* Fix #4714: Stack overflow with native computeGravatar Maxime Dénès2018-05-31
* Fix #7333: vm_compute segfaults / Anomaly with cofixGravatar Maxime Dénès2018-05-28
* Unify pre_env and envGravatar Maxime Dénès2018-05-28
* Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Fix map iterator on nativelambda.Gravatar Maxime Dénès2018-02-23
* [native_compute] Fix handling of evars in conversionGravatar Maxime Dénès2018-02-05
* Fast environment lookup for rels.Gravatar Pierre-Marie Pédrot2017-12-29
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove dead code in native compiler.Gravatar Maxime Dénès2017-05-02
* Locally disable some warnings.Gravatar Gaetan Gilbert2017-04-27
* CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* 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