aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun/coq_interp.c
AgeCommit message (Expand)Author
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-11-01Fix ldshiftexpPierre Roux
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
2019-11-01Make primitive float work on WindowsPierre 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-01Add primitive floats to 'vm_compute'Guillaume Bertholon
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
2019-04-30[vm] PPC64 registersPierre Roux
2019-04-30[vm] ARM registersPierre Roux
2019-04-30[vm] Arm 64 registersPierre Roux
2019-04-30[vm] x86_64 registersPierre Roux
2019-04-15[vm] Protect accu and coq_envPierre Roux
2019-02-04Primitive integersMaxime Dénès
2018-05-28Make some comments more precise about compilation of cofixpointsMaxime Dénès
2018-04-30Wrap VM bytecode used on the OCaml side in an OCaml block.Pierre-Marie Pédrot
2018-03-26Moving the VM global atom table to a ML reference.Pierre-Marie Pédrot
2018-03-26Moving the VM global data to a ML reference.Pierre-Marie Pédrot
2016-12-23Handle application of a primitive projection to a not yet evaluated cofixpoin...Guillaume Melquiond
2016-12-06Fix #5248 - test-suite fails in 8.6beta1Maxime Dénès
2016-11-24Fix incorrect long multiplication in the VM.Guillaume Melquiond
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-24Fix #5127 Memory corruption with the VMMaxime Dénès
2016-10-19More comments in VM.Maxime Dénès
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-31Fix potential race condition in vm_compute.Guillaume Melquiond
2016-03-25Remove int64 emulation in bytecode interpreter.Maxime Dénès
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-14Make interpreter of PROJ simpler by not using the stack.Guillaume Melquiond
2015-10-14Remove some unused variables.Guillaume Melquiond
2015-10-14Fix some typos.Guillaume Melquiond
2015-09-06Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Maxime Dénès
2015-09-06Fixed critical bug in 31 bit arithmetic of VMCatalin Hritcu
2015-07-05Fix handling of primitive projections in VM.Maxime Dénès
2015-04-27Fix some ill-typed debugging code in the VM.Guillaume Melquiond
2015-03-30fix code and bound for SWITCH instruction.Benjamin Gregoire
2015-03-26allows the vm to deal with inductive type with 8388607 constant constructors ...Benjamin Gregoire
2015-03-13Fix compilation with forthcoming Ocaml version 4.03.Arnaud Spiwack
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 21:30:57 +0000