aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
AgeCommit message (Expand)Author
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:51:18 +0000