coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/vmvalues.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

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 #21767: Qglobal is not QVar
committed
Gaëtan Gilbert
QGlobal is not QVar
committed

January 2025

coqbot-app[bot]
Merge PR #20026: Rename Coq -> Rocq in various comments and doc
committed
Pierre Roux
Rename Coq -> Rocq in various comments and doc
committed
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

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 #19034: More efficient compilation of PArray blobs in the VM.
committed
Pierre-Marie Pédrot
Allow floats in VM structured values.
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

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
Gaëtan Gilbert
Add Var constructor to qvar, move UState.quality to Sorts
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
Optimize closed universe 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

July 2023

coqbot-app[bot]
Merge PR #17719: Stop handling evars as free variables in the VM.
committed

June 2023

Pierre-Marie Pédrot
Stop handling evars as free variables in the VM.
committed
coqbot-app[bot]
Merge PR #17662: Fix sort quality variables with async workers
committed

May 2023

Gaëtan Gilbert
Fix sort quality variables with async workers
committed

February 2023

coqbot-app[bot]
Merge PR #17177: Fix some universe name printing
committed
Gaëtan Gilbert
Fix some universe name printing
committed

January 2023

coqbot-app[bot]
Merge PR #16903: Introduce sort variables in unification
committed
Pierre-Marie Pédrot
Introduce quality variables in sorts.
committed

December 2022

coqbot-app[bot]
Merge PR #16961: Clean the bytecode interpreter
committed
Guillaume Melquiond
Let coq_fix_code.c handle the ACCUMULATE closure.
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
coqbot-app[bot]
Merge PR #16640: Fix interpretation of VM/native values.
committed
Guillaume Melquiond
Remove unused code during interpretation of VM/native values.
committed