coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-13	Set the lsb of return addresses on the bytecode interpreter stack.	Guillaume Melquiond
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-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-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	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-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-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	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
2019-11-01	Change return type of primitive float comparison	Pierre Roux
2019-11-01	Add primitive floats to 'vm_compute'	Guillaume Bertholon
2019-05-15	Merge PR #9905: [vm] x86_64 registers	Maxime Dénès
2019-05-03	Remove now useless commented code	Pierre Roux
2019-05-03	[primitive integers] Make div21 implems consistent with its specification	Pierre Roux
2019-04-30	[vm] Backport from OCaml	Pierre Roux
2019-04-30	[vm] PPC64 registers	Pierre Roux
2019-04-30	[vm] ARM registers	Pierre Roux
2019-04-30	[vm] Arm 64 registers	Pierre Roux
2019-04-30	[vm] x86_64 registers	Pierre Roux
2019-04-15	[vm] Protect accu and coq_env	Pierre Roux
2019-02-04	Primitive integers	Maxime Dénès
2018-05-28	Make some comments more precise about compilation of cofixpoints	Maxime Dénès
2018-04-30	Wrap VM bytecode used on the OCaml side in an OCaml block.	Pierre-Marie Pédrot