coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-13	Make callback opcodes more generic.	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-07-22	Remove redundant data from VM case switch.	Pierre-Marie Pédrot
2020-07-06	Primitive persistent arrays	Maxime Dénès
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	Put axioms on ldshiftexp and frshiftexp	Guillaume Bertholon
2019-11-01	Add primitive floats to 'vm_compute'	Guillaume Bertholon
2019-02-04	Primitive integers	Maxime Dénès
2015-10-28	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha
2015-10-09	Code cleaning in VM (with Benjamin).	Maxime Dénès
2015-07-05	Fix handling of primitive projections in VM.	Maxime Dénès
2008-09-04	Rely on ocamlc to call the C compiler...	glondu
2006-12-11	Changement dans le kernel :	bgregoir
2006-10-27	changement des _sym par _comm dans setoid_ring	bgregoir
2006-07-22	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir
2004-10-20	COMMITED BYTECODE COMPILER	barras