coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/vm.ml

October 2026

coqbot-app[bot]
Merge PR #22652: Fix proof of False when VM conversion eta-expands a mutual fixpoint
committed
Sami Jawhar
Fix proof of False when VM conversion eta-expands a mutual fixpoint
committed

October 2024

coqbot-app[bot]
Merge PR #19721: Rocqify the VM
committed
Pierre-Marie Pédrot
Rename all C functions and macros from the VM according to the Great Rocqification.
committed
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

June 2024

coqbot-app[bot]
Merge PR #18973: Add primitive string type.
committed
Rodolphe Lepigre
Add a primitive string type.
committed

December 2022

coqbot-app[bot]
Merge PR #16961: Clean the bytecode interpreter
committed
Guillaume Melquiond
Remove the "drawinstr" infrastructure, as it is a noop.
committed

November 2022

coqbot-app[bot]
Merge PR #16629: Merge the VM and native reification view type
committed

October 2022

Pierre-Marie Pédrot
Merge the VM and native view types.
committed
coqbot-app[bot]
Merge PR #16696: Uniform naming scheme for VM kind views
committed
Pierre-Marie Pédrot
Rename the VM view kinds for constants and blocks like native.
committed
Pierre-Marie Pédrot
Rename the Vatom_stk constructor into Vaccu in the VM implementaiton.
committed
coqbot-app[bot]
Merge PR #16656: Remove the Vuniv_level constructor of VM value kinds.
committed
Pierre-Marie Pédrot
Remove the Vuniv_level constructor of VM value kinds.
committed

January 2022

coqbot-app[bot]
Merge PR #12640: Use local persistent data structures for VM global tables
committed
Pierre-Marie Pédrot
Encapsulate the only call to the VM interpreter inside Csymtable.
committed

September 2020

coqbot-app[bot]
Merge PR #12894: Modify bytecode representation of closures to please OCamls GC (fix #12636).
committed
Guillaume Melquiond
Modify bytecode representation of closures to please OCaml's GC (fix #12636).
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

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

Gaëtan Gilbert
Merge PR #11010: [coq] Untabify the whole ML codebase.
committed
Emilio Jesus Gallego Arias
[coq] Untabify the whole ML codebase.
committed
Maxime Dénès
Merge PR #9867: Add primitive floats (binary64 floating-point numbers)
committed
Guillaume Bertholon
Add primitive floats to 'vm_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

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 #7571: [kernel] Compile with almost all warnings enabled.
committed
Emilio Jesus Gallego Arias
[kernel] Compile with almost all warnings enabled.
committed
Pierre-Marie Pédrot
Merge PR #6906: [VM] Optimize structured values
committed
Maxime Dénès
[VM] Move structured_constant to Vmvalues
committed

April 2018

Maxime Dénès
Merge PR #6908: Move VM global tables from C to ML
committed

March 2018

Pierre-Marie Pédrot
Moving the VM global atom table to a ML reference.
committed
Pierre-Marie Pédrot
Moving the VM global data to a ML reference.
committed
Maxime Dénès
Merge PR #6855: Update headers following #6543.
committed
Maxime Dénès
Merge PR #935: Handling evars in the VM
committed
Maxime Dénès
Merge PR #6876: Unify Const_sorts and Const_type, and remove Vsort
committed
Pierre-Marie Pédrot
Handling evars in the VM.
committed
Maxime Dénès
[VM] Unify Const_sorts and Const_type, and remove Vsort.
committed

February 2018

Théo Zimmermann
Update headers following #6543.
committed

January 2018

Maxime Dénès
Merge PR #6605: Safer VM interfaces
committed
Maxime Dénès
Safer VM interfaces
committed