aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun
AgeCommit message (Expand)Author
2021-03-31[dune] Rename byterun to coqrunEmilio Jesus Gallego Arias
2021-03-13Set 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-26Signed primitive integersAna
2021-02-26Merge PR #13676: Protect caml_process_pending_actions_exn with caml_something...Pierre-Marie Pédrot
2021-02-19Be less permissive with respect to nonsensical bytecode.Guillaume Melquiond
2021-02-19Make the generated file the official source of arity.Guillaume Melquiond
2021-02-19Add a file coq_arity.h generated by genOpcodeFiles.ml.Guillaume Melquiond
2021-02-16Fix missing arities of VM opcodes.Guillaume Melquiond
2021-01-10Remove MAKEPROD.Guillaume Melquiond
2021-01-10Remove SETFIELD0 and SETFIELD1.Guillaume Melquiond
2021-01-10Remove LSLINT63CONST1 and LSRINT63CONST1 as they are unused.Guillaume Melquiond
2021-01-10Remove PUSHACC0, as it is strictly equivalent to PUSH.Guillaume Melquiond
2020-12-26Protect caml_process_pending_actions_exn with caml_something_to_do.Guillaume Melquiond
2020-12-01Avoid compiler warnings.Guillaume Melquiond
2020-11-20Make sure accumulators do not exceed the minor heap (partly fix #11170).Guillaume Melquiond
2020-11-13Hardcode next_up and next_down instead of relying on nextafter.Guillaume Melquiond
2020-11-13Add allocation-free variants of the nextup and nextdown floating-point operat...Guillaume Melquiond
2020-11-13Remove floating-point comparison operators as they are no longer needed.Guillaume Melquiond
2020-11-13Turn coq_float64.h into a .c file as it is no longer needed by coq_interp.c.Guillaume Melquiond
2020-11-13Inline the functions from coq_float64.h.Guillaume Melquiond
2020-11-13Make callback opcodes more generic.Guillaume Melquiond
2020-11-13Optimize Is_accu a bit.Guillaume Melquiond
2020-11-13Remove some unused opcodes from VM.Guillaume Melquiond
2020-11-13Remove unchecked arithmetic operations from VM, as they are not used.Guillaume Melquiond
2020-11-13Optimize handling of the VM stack with respect to the GC.Guillaume Melquiond
2020-09-22Use the closure tag for accumulators.Guillaume Melquiond
2020-09-22Use the same memory layout as closures for accumulators.Guillaume Melquiond
2020-09-22Modify bytecode representation of closures to please OCaml's GC (fix #12636).Guillaume Melquiond
2020-07-22Remove redundant data from VM case switch.Pierre-Marie Pédrot
2020-07-06Primitive persistent arraysMaxime Dénès
2020-03-27Merge PR #11102: Use the Alloc_small macro from the OCaml runtime rather than...Maxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-09Do not rely on the implicit declaration of caml_minor_collection.Guillaume Melquiond
2019-12-22Use the Alloc_small macro from the OCaml runtime rather than our own.Guillaume Melquiond
2019-12-17failwith -> caml_failwithGuillaume Munch-Maccagnoni
2019-12-17Fatal error in VM if SIGINT was seen but no exception occured.Guillaume Munch-Maccagnoni
2019-12-17Fix signal polling for OCaml 4.10Guillaume Munch-Maccagnoni
2019-12-17[VM] fix volatile declarationGuillaume 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.0Emilio Jesus Gallego Arias
2019-11-11Have only one dune rule calling configurePierre Roux
2019-11-01Communicate CFLAGS to dunePierre Roux
2019-11-01Fix ldshiftexpPierre Roux
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
2019-11-01Make primitive float work on WindowsPierre Roux
2019-11-01Reimplement is_floatPierre Roux
2019-11-01Make primitive float work on x86_32Pierre Roux
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
2019-11-01Implement classify on primitive floatPierre Roux