index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
vmemitcodes.ml
Age
Commit message (
Expand
)
Author
2021-02-26
Signed primitive integers
Ana
2021-01-10
Remove MAKEPROD.
Guillaume Melquiond
2021-01-10
Remove SETFIELD0 and SETFIELD1.
Guillaume Melquiond
2021-01-10
Add a peephole optimization for PUSHFIELDS(1).
Guillaume Melquiond
2021-01-10
Remove PUSHACC0, as it is strictly equivalent to PUSH.
Guillaume Melquiond
2020-11-13
Add allocation-free variants of the nextup and nextdown floating-point operat...
Guillaume Melquiond
2020-11-13
Make callback opcodes more generic.
Guillaume Melquiond
2020-11-13
Turn Ksequence into a unary opcode, as its binary structure was never used.
Guillaume Melquiond
2020-11-13
Remove some unused opcodes from VM.
Guillaume Melquiond
2020-11-13
Remove unchecked arithmetic operations from VM, as they are not used.
Guillaume Melquiond
2020-10-21
Same little game with Projection.
Pierre-Marie Pédrot
2020-10-21
Deprecate the non-qualified equality functions on kerpairs.
Pierre-Marie Pédrot
2020-10-08
Remove occurrences of Parray.reroot.
Guillaume Melquiond
2020-09-22
Modify bytecode representation of closures to please OCaml's GC (fix #12636).
Guillaume Melquiond
2020-08-18
Rename VM-related kernel/cfoo files to kernel/vmfoo
Gaëtan Gilbert