coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
*	Make kernel reduction code parametric over the handling of universes,	Matthieu Sozeau	2014-06-06
*	- Rename eq to equal in Univ, document new modules, set interfaces.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing pervasives equalities in Vconv.	Pierre-Marie Pédrot	2014-03-04
*	Conv_orable made functional and part of pre_env	gareuselesinge	2013-10-31
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Propagated information from the reduction tactics to the kernel so	herbelin	2011-08-10
*	adding eta in the vm	bgregoir	2011-03-08
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin	2006-10-05
*	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir	2006-07-22
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	correction bug 881.	gregoire	2005-12-05
*	Changement des named_context	gregoire	2005-12-02
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Types inductifs parametriques	mohring	2005-11-02
*	Uniformisation de destApplication en destApp	herbelin	2005-02-12
*	Code mort	herbelin	2004-11-22
*	compatibility with POWERPC	gregoire	2004-11-22
*	Changement dans les boxed values .	gregoire	2004-11-12
*	COMMITED BYTECODE COMPILER	barras	2004-10-20