coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/vmvalues.mli

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

January 2025

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
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
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
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

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

December 2021

coqbot-app[bot]
Merge PR #15401: Use anonymous primitive projections in the VM.
committed
Pierre-Marie Pédrot
Use anonymous primitive projections in the VM.
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 #14007: Never store persistent arrays as VM structured values.
committed
Pierre-Marie Pédrot
Never store persistent arrays as VM structured values.
committed

October 2020

coqbot-app[bot]
Merge PR #12955: Reroot primitive arrays on access
committed
Guillaume Melquiond
Remove occurrences of Parray.reroot.
committed

September 2020

coqbot-app[bot]
Merge PR #12894: Modify bytecode representation of closures to please OCamls GC (fix #12636).
committed
Guillaume Melquiond
Use the closure tag for accumulators.
committed
Guillaume Melquiond
Modify bytecode representation of closures to please OCaml's GC (fix #12636).
committed

July 2020

Gaëtan Gilbert
Merge PR #12679: Remove redundant data from VM case switch.
committed
Pierre-Marie Pédrot
Remove redundant data from VM case switch.
committed
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

Maxime Dénès
Merge PR #9867: Add primitive floats (binary64 floating-point numbers)
committed