aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun
AgeCommit message (Expand)Author
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-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
2019-11-01Change return type of primitive float comparisonPierre Roux
2019-11-01Put axioms on ldshiftexp and frshiftexpGuillaume Bertholon
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
2019-07-29Use the precondition of diveucl_21 to avoid massaging the dividend.Guillaume Melquiond
2019-07-29Use a more traditional definition for uint63_div21 (fixes #10551).Guillaume Melquiond
2019-05-23Fixing typos - Part 2JPR
2019-05-15Merge PR #9905: [vm] x86_64 registersMaxime Dénès
2019-05-03Remove now useless commented codePierre Roux
2019-05-03[primitive integers] Make div21 implems consistent with its specificationPierre Roux
2019-04-30[vm] Backport from OCamlPierre Roux