coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/vmbytegen.ml

September 2026

coqbot-app[bot]
Merge PR #21196: Be more defensive against nullary functions (cf #21136).
committed
Guillaume Melquiond
Be more defensive against nullary functions (cf #21136).
committed
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

March 2026

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
coqbot-app[bot]
Merge PR #21767: Qglobal is not QVar
committed
Gaëtan Gilbert
QGlobal is not QVar
committed
Gaëtan Gilbert
Vmbytegen.compile return None if VM disabled
committed

December 2025

coqbot-app[bot]
Merge PR #21405: Perform kernel typing after universe abstraction for polymorphic code.
committed
Pierre-Marie Pédrot
Allow bound universe variables in the VM.
committed

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

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

July 2024

coqbot-app[bot]
Merge PR #19392: Newprofile: profile vm_compile component
committed
Gaëtan Gilbert
Newprofile: profile vm_compile component
committed

June 2024

coqbot-app[bot]
Merge PR #18973: Add primitive string type.
committed
Rodolphe Lepigre
Add a primitive string type.
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 #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 #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

April 2024

coqbot-app[bot]
Merge PR #18968: Use callback to substitute universe instances in VM
committed
Gaëtan Gilbert
Use callback to substitute universe instances in VM
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

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
coqbot-app[bot]
Merge PR #18038: Add rewrite rules to Coq
committed
Yann Leray
Add symbols, patterns, rewrite rule fields
committed

November 2023

coqbot-app[bot]
Merge PR #18340: Fix const_relevance and default qvar handler with sort polymorphism
committed
Gaëtan Gilbert
qvar_irrelevant in default_evar_handler: assert that the qvar is known
committed
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
Gaëtan Gilbert
Move universe polymorphism APIs to new file UVars before sort poly
committed

September 2023

coqbot-app[bot]
Merge PR #17926: Pass bound universes directly as an instance in the VM.
committed
Pierre-Marie Pédrot
Fix max stack size computation in VM instance compilation.
committed
Pierre-Marie Pédrot
Optimize closed universe instances in VM compilation.
committed
Pierre-Marie Pédrot
Optimize identity instances in VM compilation.
committed
Pierre-Marie Pédrot
Further simplification of sort compilation in the VM.
committed
Pierre-Marie Pédrot
Pass bound universes directly as an instance in the VM.
committed