coq - The formal proof system

Age	Commit message (Expand)	Author
2020-07-06	Primitive persistent arrays	Maxime Dénès
2019-12-12	[vm] Untabify the VM C code.	Emilio Jesus Gallego Arias
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-02-04	Primitive integers	Maxime Dénès
2018-04-30	Wrap VM bytecode used on the OCaml side in an OCaml block.	Pierre-Marie Pédrot
2016-10-24	Fix #5127 Memory corruption with the VM	Maxime Dénès
2015-07-05	Fix handling of primitive projections in VM.	Maxime Dénès
2015-03-30	fix code and bound for SWITCH instruction.	Benjamin Gregoire
2015-03-26	allows the vm to deal with inductive type with 8388607 constant constructors ...	Benjamin Gregoire
2015-03-13	Fix compilation with forthcoming Ocaml version 4.03.	Arnaud Spiwack
2012-10-02	Remove some dead code in the vm	letouzey
2012-08-11	fast bitwise operations (lor,land,lxor) on int31 and BigN	letouzey
2008-09-04	Rely on ocamlc to call the C compiler...	glondu
2007-06-20	ajout de head0 et tail0 en natif	bgregoir
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
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