aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun/coq_fix_code.c
AgeCommit message (Expand)Author
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-11-13Make callback opcodes more generic.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-09-22Modify bytecode representation of closures to please OCaml's GC (fix #12636).Guillaume Melquiond
2020-07-06Primitive persistent arraysMaxime Dénès
2019-12-12[vm] Untabify the VM C code.Emilio Jesus Gallego Arias
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
2019-11-01Implement classify on primitive floatPierre Roux
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
2019-02-04Primitive integersMaxime Dénès
2018-04-30Wrap VM bytecode used on the OCaml side in an OCaml block.Pierre-Marie Pédrot
2016-10-24Fix #5127 Memory corruption with the VMMaxime Dénès
2015-07-05Fix handling of primitive projections in VM.Maxime Dénès
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
2012-10-02Remove some dead code in the vmletouzey
2012-08-11fast bitwise operations (lor,land,lxor) on int31 and BigNletouzey
2008-09-04Rely on ocamlc to call the C compiler...glondu
2007-06-20ajout de head0 et tail0 en natifbgregoir
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2006-12-11Changement dans le kernel : bgregoir
2006-07-22- Ajout d'un cast vm dans la syntaxe : x <: t bgregoir
2004-11-22compatibility with POWERPCgregoire
2004-11-12Changement dans les boxed values .gregoire
2004-10-20COMMITED BYTECODE COMPILERbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:59:45 +0000