coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/vmlambda.mli

May 2025

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

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

May 2024

coqbot-app[bot]
Merge PR #19034: More efficient compilation of PArray blobs in the VM.
committed
Pierre-Marie Pédrot
More efficient compilation of PArray blobs in the VM.
committed
coqbot-app[bot]
Merge PR #19015: Factor the lambda compilation passes of VM and native
committed
Pierre-Marie Pédrot
Remove the unused optimization flag for the VM compilation.
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

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 #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
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 #16480: Generalize kernel evar handling
committed
Pierre-Marie Pédrot
Wrap the evar expander type into an explicit record.
committed

May 2021

Théo Zimmermann
Add examples from former detailed tactic examples chapter to their new location.
committed

March 2021

coqbot-app[bot]
Merge PR #13854: Normalize evars during bytecode compilation.
committed

February 2021

Guillaume Melquiond
Normalize evars during bytecode compilation (fix #13841).
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
Guillaume Melquiond
Remove unchecked arithmetic operations from VM, as they are not used.
committed

August 2020

Pierre-Marie Pédrot
Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfoo
committed
Gaëtan Gilbert
Rename VM-related kernel/cfoo files to kernel/vmfoo
committed