coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/vmemitcodes.ml

September 2026

coqbot-app[bot]
Merge PR #22437: Treat opaque Var nodes as structured constants in the VM.
committed
Pierre-Marie Pédrot
Treat opaque Var nodes as structured constants in the VM.
committed

April 2026

coqbot-app[bot]
Merge PR #21856: Stop relying on canonical names in VM internals.
committed

March 2026

Pierre-Marie Pédrot
Stop relying on canonical names in VM internals.
committed
coqbot-app[bot]
Merge PR #21677: Improved handling of disabled VM
committed
Gaëtan Gilbert
VM error when encountering non compiled constant (from disabled VM)
committed

May 2025

coqbot-app[bot]
Merge PR #20584: Use APIs new since ocaml 4.09
committed
Gaëtan Gilbert
Use APIs new since ocaml 4.09
committed
Gaëtan Gilbert
Use String.get_int32_be in vmemitcodes
committed

March 2025

coqbot-app[bot]
Merge PR #20344: Hashconsing try to avoid recomputing hashes
committed
Gaëtan Gilbert
Hashconsing try to avoid recomputing hashes
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
Statically enforce primitive string size invariant.
committed
Rodolphe Lepigre
Add a primitive string type.
committed

May 2024

coqbot-app[bot]
Merge PR #18959: Compress the compiled bytecode.
committed
Guillaume Melquiond
Compress the compiled bytecode.
committed
Guillaume Melquiond
Change byte ordering of the SWITCH opcode.
committed
coqbot-app[bot]
Merge PR #18967: Add a PUSHACCMANY opcode.
committed
coqbot-app[bot]
Merge PR #18964: Add a PUSHENVACCMANY opcode.
committed
Guillaume Melquiond
Add a PUSHACCMANY opcode.
committed
Guillaume Melquiond
Add a PUSHENVACCMANY opcode.
committed
coqbot-app[bot]
Merge PR #19014: Track unused constant arguments in Genlambda and erase them.
committed
Pierre-Marie Pédrot
Track unused constant arguments in Genlambda and erase them.
committed
coqbot-app[bot]
Merge PR #18718: Store VM relocations that do not need substitution on disk.
committed
Pierre-Marie Pédrot
Store VM relocations that do not need substitution on disk.
committed

April 2024

coqbot-app[bot]
Merge PR #18968: Use callback to substitute universe instances in VM
committed
Gaëtan Gilbert
Cleanup unused structured constant kinds after coq_subst_instance
committed
Gaëtan Gilbert
Use callback to substitute universe instances in VM
committed

February 2024

coqbot-app[bot]
Merge PR #17674: Store VM bytecode in a dedicated vo segment
committed
Pierre-Marie Pédrot
Small reorganization of the to_patch data type.
committed

November 2023

coqbot-app[bot]
Merge PR #17836: Kernel sort polymorphism
committed
Gaëtan Gilbert
sort poly (with simple squashing model and no inductive output in qsort)
committed

September 2023

coqbot-app[bot]
Merge PR #17926: Pass bound universes directly as an instance in the VM.
committed
Pierre-Marie Pédrot
Optimize closed universe instances in VM compilation.
committed

July 2023

coqbot-app[bot]
Merge PR #17719: Stop handling evars as free variables in the VM.
committed
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

June 2023

Pierre-Marie Pédrot
Stop handling evars as free variables in the VM.
committed
coqbot-app[bot]
Merge PR #17668: Only keep projection index in Kproj VM bytecode.
committed

May 2023

Pierre-Marie Pédrot
Only keep projection index in Kproj VM bytecode.
committed

December 2022

coqbot-app[bot]
Merge PR #16985: More compact representation of VM patch positions.
committed
Pierre-Marie Pédrot
Clean up int32-related code in Vmemitcodes.
committed
Pierre-Marie Pédrot
Simplify the representation of VM positions.
committed
Pierre-Marie Pédrot
Store relocations directly in the VM bytecode.
committed
Pierre-Marie Pédrot
More compact representation of VM patch positions.
committed

November 2022

coqbot-app[bot]
Merge PR #16848: Fix representation of empty arrays (fix #16832).
committed