coq - The formal proof system

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