aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-01Add primitive floats to 'native_compute'Pierre Roux
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-04-15[native compiler] Encoding of constructors based on tagsMaxime Dénès
2019-04-15[native compiler] Remove unused universe argument in LmakeblockMaxime Dénès
2019-04-15[native compiler] Distinguish constant constructors in lambda codeMaxime Dénès
2019-04-14[native compiler] Remove `Lconstruct` from lambda code.Maxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-09-14Retroknowledge: use GlobRef.t instead of Constr.t as entryVincent Laporte
2018-07-26Fix #8121: anomalies in native_compute with let and evars.Pierre-Marie Pédrot
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-13Store the {struct} inductive type in native fixpoint AST.Pierre-Marie Pédrot
2018-07-13Pass a proper environment to Nativelambda.lambda_of_constr.Pierre-Marie Pédrot
2018-06-28[env.env_rel_context.env_rel_ctx] -> [rel_context env]Gaëtan Gilbert
2018-06-24Merge PR #7772: [native_compute] Delay computations with toplevel matchPierre-Marie Pédrot
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
2018-06-11[native_compute] Delay computations with toplevel matchMaxime Dénès
2018-06-05Use projection indices in native compilation rather than constant names.Pierre-Marie Pédrot
2018-05-31Fix #4714: Stack overflow with native computeMaxime Dénès
2018-05-28Fix #7333: vm_compute segfaults / Anomaly with cofixMaxime Dénès
2018-05-28Unify pre_env and envMaxime Dénès
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-23Fix map iterator on nativelambda.Maxime Dénès
2018-02-05[native_compute] Fix handling of evars in conversionMaxime Dénès
2017-12-29Fast environment lookup for rels.Pierre-Marie Pédrot
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-02Remove dead code in native compiler.Maxime Dénès
2017-04-27Locally disable some warnings.Gaetan Gilbert
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Avoid warnings about loop indices.Guillaume Melquiond
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-13Fix some typos.Guillaume Melquiond
2015-07-29Fixing some English misspelling.Hugo Herbelin
2015-03-25Fix vm compiler to refuse to compile code making use of inductives withMatthieu Sozeau
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-15Correct restriction of vm_compute when handling universe polymorphicMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:28:04 +0000