coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Refine Gregory Malecha's patch on VM and universe polymorphism.	Maxime Dénès	2015-10-28
*	Adds support for the virtual machine to perform reduction of universe polymor...	Gregory Malecha	2015-10-28
*	Gather VM tags in Cbytecodes.	Maxime Dénès	2015-10-12
*	Complete handling of primitive projections in VM.	Maxime Dénès	2015-10-09
*	Code cleaning in VM (with Benjamin).	Maxime Dénès	2015-10-09
*	Fix handling of primitive projections in VM.	Maxime Dénès	2015-07-05
*	use a more compact representation of non-constant constructors	Benjamin Gregoire	2015-03-27
*	Fix bug 4157,	Benjamin Gregoire	2015-03-26
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Fixing generic hashes and replacing them with proper ones.	Pierre-Marie Pédrot	2014-03-03
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Remove some dead code in the vm	letouzey	2012-10-02
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Noise for nothing	pboutill	2012-03-02
*	adding eta in the vm	bgregoir	2011-03-08
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	better fix to bug #2319: types are compiled in the env of the bodies	barras	2010-07-30
*	fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodies	barras	2010-07-28
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	removed a potentially dangerous try ... with _ -> ...	barras	2010-07-16
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move Obj.magic call to the Vm module	glondu	2009-11-13
*	Removal of trailing spaces.	serpyc	2009-10-04
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
*	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin	2007-01-19
*	Changement dans le kernel :	bgregoir	2006-12-11
*	correction bug vm_compute	bgregoir	2006-08-25
*	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir	2006-07-22
*	changement d'egalite pour le named_context_val	gregoire	2005-12-05
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	compatibility with POWERPC	gregoire	2004-11-22
*	Changement dans les boxed values .	gregoire	2004-11-12
*	COMMITED BYTECODE COMPILER	barras	2004-10-20