coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/vmbytecodes.mli

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

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

September 2023

coqbot-app[bot]
Merge PR #17926: Pass bound universes directly as an instance 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 #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

January 2022

coqbot-app[bot]
Merge PR #12640: Use local persistent data structures for VM global tables
committed
Pierre-Marie Pédrot
Statically capture VM primitives implemented directly in OCaml.
committed

May 2021

Théo Zimmermann
Add examples from former detailed tactic examples chapter to their new location.
committed

March 2021

Pierre-Marie Pédrot
Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.
committed
Guillaume Melquiond
Make it more obvious when the calling convention of APPLY changes.
committed

January 2021

Pierre-Marie Pédrot
Merge PR #13678: Cleaning up the bytecode interpreter
committed
Guillaume Melquiond
Remove MAKEPROD.
committed

November 2020

Pierre-Marie Pédrot
Merge PR #12959: Improve the bytecode interpreter
committed
Guillaume Melquiond
Turn Ksequence into a unary opcode, as its binary structure was never used.
committed
Guillaume Melquiond
Remove some unused opcodes from VM.
committed
Guillaume Melquiond
Remove unchecked arithmetic operations from VM, as they are not used.
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