coq - The formal proof system

Age	Commit message (Expand)	Author
2021-02-19	Add a file coq_arity.h generated by genOpcodeFiles.ml.	Guillaume Melquiond
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-11-13	Add allocation-free variants of the nextup and nextdown floating-point operat...	Guillaume Melquiond
2020-11-13	Make callback opcodes more generic.	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-09-22	Modify bytecode representation of closures to please OCaml's GC (fix #12636).	Guillaume Melquiond
2020-08-18	Rename VM-related kernel/cfoo files to kernel/vmfoo	Gaëtan Gilbert
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-11-01	Add "==", "<", "<=" in PrimFloat.v	Erik Martin-Dorel
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	Add primitive floats to 'vm_compute'	Guillaume Bertholon
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-03-01	[Kernel] Simpler generation of opcode files	Vincent Laporte