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-19	Make the generated file the official source of arity.	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
2019-12-22	Use the Alloc_small macro from the OCaml runtime rather than our own.	Guillaume Melquiond
2019-12-12	[vm] Untabify the VM C code.	Emilio Jesus Gallego Arias
2019-05-23	Fixing typos - Part 2	JPR
2018-04-30	Adapt the VM GC hook to handle the no-naked-pointers option flag.	Pierre-Marie Pédrot
2018-04-30	Make the VM accumulator look like an OCaml block.	Pierre-Marie Pédrot
2018-04-30	Wrap VM bytecode used on the OCaml side in an OCaml block.	Pierre-Marie Pédrot
2018-03-26	Moving the VM global atom table to a ML reference.	Pierre-Marie Pédrot
2018-03-26	Moving the VM global data to a ML reference.	Pierre-Marie Pédrot
2016-10-24	Fix #5127 Memory corruption with the VM	Maxime Dénès
2015-10-14	Remove some unused variables.	Guillaume Melquiond
2015-10-09	Code cleaning in VM (with Benjamin).	Maxime Dénès
2012-10-02	Remove some dead code in the vm	letouzey
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2006-12-11	Changement dans le kernel :	bgregoir
2006-07-22	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir
2004-11-22	compatibility with POWERPC	gregoire
2004-11-12	Changement dans les boxed values .	gregoire
2004-10-20	COMMITED BYTECODE COMPILER	barras