coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/nativelambda.mli

October 2024

coqbot-app[bot]
Merge PR #19692: Update the OCaml headers to reflect the fact Coq is now Rocq.
committed
Pierre-Marie Pédrot
Update the OCaml headers to reflect the fact Coq is now Rocq.
committed

March 2024

coqbot-app[bot]
Merge PR #18692: Remove the Lforce node from the generic lambda AST.
committed
Pierre-Marie Pédrot
Remove the Lforce node from the generic lambda AST.
committed

November 2022

coqbot-app[bot]
Merge PR #16780: Share the Lambda code generation phase in VM and native compilation
committed
Pierre-Marie Pédrot
Move prefix-related code from Nativelambda to Nativecode.
committed
coqbot-app[bot]
Merge PR #16671: Share the VM and native lambda AST in a single type.
committed

October 2022

Pierre-Marie Pédrot
Additional sharing of some lambda code.
committed
Pierre-Marie Pédrot
Share some utility functions on the Genlambda type.
committed
Pierre-Marie Pédrot
Share the VM and native lambda AST in a single type.
committed
Pierre-Marie Pédrot
Simplify the case annotation type stored in native lambda AST.
committed
Pierre-Marie Pédrot
Tweak the Lproj native constructor to look like the VM one.
committed
Pierre-Marie Pédrot
Remove the unused Lif constructor from Nativelambda.lambda.
committed
Pierre-Marie Pédrot
Remove the unused Lrec constructor from Nativelambda.lambda.
committed
Pierre-Marie Pédrot
Move the prefix computation from lambda phase to code in native compiler.
committed

September 2022

coqbot-app[bot]
Merge PR #16480: Generalize kernel evar handling
committed
Pierre-Marie Pédrot
Wrap the evar expander type into an explicit record.
committed

May 2022

coqbot-app[bot]
Merge PR #16017: Cleanup of native compilation
committed
Pierre-Marie Pédrot
Fix the compilation of lazy values in native compiler.
committed

July 2020

Pierre-Marie Pédrot
Merge PR #11604: Primitive persistent arrays
committed
Maxime Dénès
Primitive persistent arrays
committed

March 2020

Hugo Herbelin
Merge PR #11559: Remove year in headers.
committed
Théo Zimmermann
Update headers in the whole code base.
committed

November 2019

Maxime Dénès
Merge PR #9867: Add primitive floats (binary64 floating-point numbers)
committed
Pierre Roux
Add primitive floats to 'native_compute'
committed

June 2019

Clément Pit-Claudel
Merge PR #10320: Update headers to the new year.
committed
Théo Zimmermann
Update ml-style headers to new year.
committed

April 2019

Pierre-Marie Pédrot
Merge PR #9962: [native compiler] Encoding of constructors based on tags
committed
Maxime Dénès
[native compiler] Encoding of constructors based on tags
committed
Maxime Dénès
[native compiler] Remove unused universe argument in Lmakeblock
committed
Maxime Dénès
[native compiler] Distinguish constant constructors in lambda code
committed
Pierre-Marie Pédrot
Merge PR #9959: [native compiler] Remove `Lconstruct` from lambda code.
committed
Maxime Dénès
[native compiler] Remove `Lconstruct` from lambda code.
committed

March 2019

Pierre-Marie Pédrot
Merge PR #8817: SProp: the definitionally proof irrelevant universe
committed
Gaëtan Gilbert
Add relevance marks on binders.
committed

February 2019

Pierre-Marie Pédrot
Merge PR #6914: Primitive integers
committed
Maxime Dénès
Primitive integers
committed

September 2018

Maxime Dénès
Merge PR #8124: Fix #8121: anomalies in native_compute with let and evars.
committed

July 2018

Pierre-Marie Pédrot
Fix #8121: anomalies in native_compute with let and evars.
committed
Maxime Dénès
Merge PR #8055: Fast accumulator check in native compilation
committed
Pierre-Marie Pédrot
Pass a proper environment to Nativelambda.lambda_of_constr.
committed

May 2018

Pierre-Marie Pédrot
Merge PR #7521: Fix soundness bug with VM/native and cofixpoints
committed
Maxime Dénès
Unify pre_env and env
committed

March 2018

Maxime Dénès
Merge PR #6855: Update headers following #6543.
committed

February 2018

Théo Zimmermann
Update headers following #6543.
committed

November 2017

Maxime Dénès
Merge PR #6098: [api] Move structures deprecated in the API to the core.
committed
Maxime Dénès
Merge PR #6065: [api] Deprecate all legacy uses of Names in core.
committed
Emilio Jesus Gallego Arias
[api] Move structures deprecated in the API to the core.
committed
Emilio Jesus Gallego Arias
[api] Deprecate all legacy uses of Names in core.
committed

August 2017

Maxime Dénès
Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.
committed