coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/vmlambda.ml

June 2025

coqbot-app[bot]
Merge PR #20690: Wrap Lambda nodes in a dummy indirection.
committed

May 2025

Pierre-Marie Pédrot
Wrap Lambda nodes in a dummy indirection.
committed
coqbot-app[bot]
Merge PR #20607: Use CDebug for Dump Bytecode and Dump Lambda
committed
Gaëtan Gilbert
Use CDebug for Dump Bytecode and Dump Lambda
committed

January 2025

coqbot-app[bot]
Merge PR #19990: VM/native: primitive strings can be included in values
committed
Gaëtan Gilbert
VM/native: primitive strings can be included in values
committed

May 2024

coqbot-app[bot]
Merge PR #19034: More efficient compilation of PArray blobs in the VM.
committed
Pierre-Marie Pédrot
Allow floats in VM structured values.
committed
coqbot-app[bot]
Merge PR #19015: Factor the lambda compilation passes of VM and native
committed
Pierre-Marie Pédrot
Use the same optimization passes for the VM and native.
committed
Pierre-Marie Pédrot
Remove the unused optimization flag for the VM compilation.
committed
Pierre-Marie Pédrot
Use the same criterion in the VM and native for substitutable atoms.
committed

March 2024

coqbot-app[bot]
Merge PR #18755: Hashcons VM structured values stored on disk.
committed
Pierre-Marie Pédrot
Hashcons VM structured values stored on disk.
committed
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

July 2023

coqbot-app[bot]
Merge PR #17752: Refactor VM error handling and catch error from generating too large code
committed
Gaëtan Gilbert
Refactor VM error handling and catch error from generating too large code
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
Factorize the lambda_of_constr function in Genlambda.
committed
Pierre-Marie Pédrot
Factorize the makeblock function in Genlambda.
committed
Pierre-Marie Pédrot
Factorize the expand_constructor function in Genlambda.
committed
Pierre-Marie Pédrot
Use a kernel environment instead of a special-purpose structure in VM compilation.
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
Move remove_let from Vlambda to Genlambda.
committed
Pierre-Marie Pédrot
Carefully share the simplify operation in Genlambda.
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
Sprinkle the VM lambda type with useless information.
committed
Pierre-Marie Pédrot
Introduce a Lmeta node in the VM lambda representation.
committed
Pierre-Marie Pédrot
Introduce a dedicated Lparray node in the VM lambda representation.
committed

September 2022

coqbot-app[bot]
Merge PR #16442: Introduce a dedicated type for evar instances.
committed
Pierre-Marie Pédrot
Introduce a dedicated type for evar instances.
committed
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 2021

coqbot-app[bot]
Merge PR #14337: Remove the delayed name substitution mechanism from the kernel
committed
Théo Zimmermann
Add examples from former detailed tactic examples chapter to their new location.
committed
Pierre-Marie Pédrot
Remove the useless to_patch_substituted indirection.
committed
Pierre-Marie Pédrot
Eagerly perform substitution in constant bodies.
committed

March 2021

coqbot-app[bot]
Merge PR #14007: Never store persistent arrays as VM structured values.
committed
Pierre-Marie Pédrot
Never store persistent arrays as VM structured values.
committed
coqbot-app[bot]
Merge PR #13854: Normalize evars during bytecode compilation.
committed

February 2021

Guillaume Melquiond
Normalize evars during bytecode compilation (fix #13841).
committed

January 2021

coqbot-app[bot]
Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)
committed
Pierre-Marie Pédrot
Change the representation of kernel case.
committed

December 2020

coqbot-app[bot]
Merge PR #13537: More efficient implementation for substitutions.
committed
Pierre-Marie Pédrot
Optimization: take advantage that we don't use arrays anymore in substitutions.
committed

November 2020

Pierre-Marie Pédrot
Merge PR #12959: Improve the bytecode interpreter
committed
Guillaume Melquiond
Remove unused if-then-else construct from VM.
committed