coq - The formal proof system

Age	Commit message (Expand)	Author
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot
2012-03-02	Noise for nothing	pboutill
2011-08-08	Esubst: make types of substitutions & lifts private	puech
2011-02-17	- Use transparency information all the way through unification and	msozeau
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-20	Added eta-expansion in kernel, type inference and tactic unification,	herbelin
2010-07-28	ported r13340 to trunk	barras
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-05-09	Added a few informations about file lineages (for the most part in kernel)	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-04-08	Some dead code removal + cleanups	letouzey
2009-02-06	pushed evar reduction in kernel	barras
2008-04-20	Add the ability to give a transparent_state for conversion, to	msozeau
2008-03-10	fold travaille maintenant sur la forme beta-iota-zeta réduite du	herbelin
2007-07-12	normalisation (by closure) was not performed under fixpoints	barras
2006-10-05	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin
2006-05-10	correction bugs dans Cbv (beta n-aire)	barras
2006-05-09	subst. explicites avec vecteurs	barras
2006-05-05	amelioration de la machine interpretee (vecteurs au lieu de listes d'arguments)	barras
2006-05-03	bug #1096: whd_stack on one arg of conversion had side-effect on the other arg	barras
2005-12-02	Changement des named_context	gregoire
2005-11-18	petites corrections + contournement bug projections	barras
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-08-22	argument inutilisÃ© de zip: toujours l'identitÃ©	letouzey
2005-07-13	reactivation de l optim des fermetures	barras
2005-07-13	backtrack modif de knh...	barras
2005-07-12	test du tag de reduction	barras
2004-11-16	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-07-16	Nouvelle en-tête	herbelin
2003-08-06	Ajout de l'opti des fermeture (mais debranche pour l'instant)	barras
2003-08-05	Improved reduction machine with closure: should use less memory	barras
2003-04-16	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-10-15	pattern-matching avec cas inutilise dans closure	barras
2002-08-16	Strengthenning rules for modules + No modules in sections	coq
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-03-12	open Univ inutile	courant
2002-01-30	cosmetique	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-05	GROS COMMIT:	barras
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-09-20	Transparent	barras
2001-09-05	Version de la reduction dans Closure plus econome en memoire:	barras
2001-07-21	Nettoyage	herbelin
2001-07-21	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin