coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/genOpcodeFiles.ml

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
Pierre-Marie Pédrot
Rename the VM C files 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 #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

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

April 2023

remzi
Merge remote-tracking branch 'upstream/master' into 17060_RelationPairs
committed
coqbot-app[bot]
Merge PR #17293: Enable warning 70 (missing mli), add mli files
committed
Gaëtan Gilbert
Enable warning 70 (missing mli), add mli files
committed

February 2022

coqbot-app[bot]
Merge PR #15719: Add primitive floating-point Leibniz equality test
committed
Pierre Roux
Add floating-point Leibniz equality primitive
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

February 2021

coqbot-app[bot]
Merge PR #13559: Signed primitive integers
committed
Ana
Signed primitive integers
committed
Pierre-Marie Pédrot
Merge PR #13868: Make genOpcodeFiles.ml handle opcode arity.
committed
Guillaume Melquiond
Make the generated file the official source of arity.
committed
Guillaume Melquiond
Add a file coq_arity.h generated by genOpcodeFiles.ml.
committed

January 2021

Pierre-Marie Pédrot
Merge PR #13678: Cleaning up the bytecode interpreter
committed
Guillaume Melquiond
Remove MAKEPROD.
committed
Guillaume Melquiond
Remove SETFIELD0 and SETFIELD1.
committed
Guillaume Melquiond
Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused.
committed
Guillaume Melquiond
Remove PUSHACC0, as it is strictly equivalent to PUSH.
committed

November 2020

Pierre-Marie Pédrot
Merge PR #12959: Improve the bytecode interpreter
committed
Guillaume Melquiond
Add allocation-free variants of the nextup and nextdown floating-point operations.
committed
Guillaume Melquiond
Make callback opcodes more generic.
committed
Guillaume Melquiond
Remove some unused opcodes from VM.
committed
Guillaume Melquiond
Remove unchecked arithmetic operations from VM, as they are not used.
committed

September 2020

coqbot-app[bot]
Merge PR #12894: Modify bytecode representation of closures to please OCamls GC (fix #12636).
committed
Guillaume Melquiond
Modify bytecode representation of closures to please OCaml's GC (fix #12636).
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

July 2020

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
Erik Martin-Dorel
Add "==", "<", "<=" in PrimFloat.v
committed
Pierre Roux
Add next_{up,down} primitive float functions
committed
Pierre Roux
Implement classify on primitive float
committed
Guillaume Bertholon
Add primitive floats to 'vm_compute'
committed

June 2019

Clément Pit-Claudel
Merge PR #10320: Update headers to the new year.
committed