index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
byterun
Age
Commit message (
Expand
)
Author
2021-03-31
[dune] Rename byterun to coqrun
Emilio Jesus Gallego Arias
2021-03-13
Set the lsb of return addresses on the bytecode interpreter stack.
Guillaume Melquiond
2021-03-03
[build] Split stdlib to it's own opam package.
Emilio Jesus Gallego Arias
2021-02-26
Signed primitive integers
Ana
2021-02-26
Merge PR #13676: Protect caml_process_pending_actions_exn with caml_something...
Pierre-Marie Pédrot
2021-02-19
Be less permissive with respect to nonsensical bytecode.
Guillaume Melquiond
2021-02-19
Make the generated file the official source of arity.
Guillaume Melquiond
2021-02-19
Add a file coq_arity.h generated by genOpcodeFiles.ml.
Guillaume Melquiond
2021-02-16
Fix missing arities of VM opcodes.
Guillaume Melquiond
2021-01-10
Remove MAKEPROD.
Guillaume Melquiond
2021-01-10
Remove SETFIELD0 and SETFIELD1.
Guillaume Melquiond
2021-01-10
Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused.
Guillaume Melquiond
2021-01-10
Remove PUSHACC0, as it is strictly equivalent to PUSH.
Guillaume Melquiond
2020-12-26
Protect caml_process_pending_actions_exn with caml_something_to_do.
Guillaume Melquiond
2020-12-01
Avoid compiler warnings.
Guillaume Melquiond
2020-11-20
Make sure accumulators do not exceed the minor heap (partly fix #11170).
Guillaume Melquiond
2020-11-13
Hardcode next_up and next_down instead of relying on nextafter.
Guillaume Melquiond
2020-11-13
Add allocation-free variants of the nextup and nextdown floating-point operat...
Guillaume Melquiond
2020-11-13
Remove floating-point comparison operators as they are no longer needed.
Guillaume Melquiond
2020-11-13
Turn coq_float64.h into a .c file as it is no longer needed by coq_interp.c.
Guillaume Melquiond
2020-11-13
Inline the functions from coq_float64.h.
Guillaume Melquiond
2020-11-13
Make callback opcodes more generic.
Guillaume Melquiond
2020-11-13
Optimize Is_accu a bit.
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-11-13
Optimize handling of the VM stack with respect to the GC.
Guillaume Melquiond
2020-09-22
Use the closure tag for accumulators.
Guillaume Melquiond
2020-09-22
Use the same memory layout as closures for accumulators.
Guillaume Melquiond
2020-09-22
Modify bytecode representation of closures to please OCaml's GC (fix #12636).
Guillaume Melquiond
2020-07-22
Remove redundant data from VM case switch.
Pierre-Marie Pédrot
2020-07-06
Primitive persistent arrays
Maxime Dénès
2020-03-27
Merge PR #11102: Use the Alloc_small macro from the OCaml runtime rather than...
Maxime Dénès
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-03-09
Do not rely on the implicit declaration of caml_minor_collection.
Guillaume Melquiond
2019-12-22
Use the Alloc_small macro from the OCaml runtime rather than our own.
Guillaume Melquiond
2019-12-17
failwith -> caml_failwith
Guillaume Munch-Maccagnoni
2019-12-17
Fatal error in VM if SIGINT was seen but no exception occured.
Guillaume Munch-Maccagnoni
2019-12-17
Fix signal polling for OCaml 4.10
Guillaume Munch-Maccagnoni
2019-12-17
[VM] fix volatile declaration
Guillaume Munch-Maccagnoni
2019-12-12
[vm] Untabify the VM C code.
Emilio Jesus Gallego Arias
2019-12-04
[dune] Update to dune language version 2.0
Emilio Jesus Gallego Arias
2019-11-11
Have only one dune rule calling configure
Pierre Roux
2019-11-01
Communicate CFLAGS to dune
Pierre Roux
2019-11-01
Fix ldshiftexp
Pierre Roux
2019-11-01
Add "==", "<", "<=" in PrimFloat.v
Erik Martin-Dorel
2019-11-01
Make primitive float work on Windows
Pierre Roux
2019-11-01
Reimplement is_float
Pierre Roux
2019-11-01
Make primitive float work on x86_32
Pierre Roux
2019-11-01
Add next_{up,down} primitive float functions
Pierre Roux
2019-11-01
Implement classify on primitive float
Pierre Roux
[next]