coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Noise for nothing	pboutill	2012-03-02
*	avoid relying on weak invariant in cbv.ml	bgregoir	2011-11-25
*	Esubst: make types of substitutions & lifts private	puech	2011-08-08
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	fixed CBV strategy: it was too eager on terms like	barras	2009-04-21
*	pushed evar reduction in kernel	barras	2009-02-06
*	correction bugs dans Cbv (beta n-aire)	barras	2006-05-10
*	subst. explicites avec vecteurs	barras	2006-05-09
*	Changement des named_context	gregoire	2005-12-02
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...	letouzey	2003-04-16
*	Nouveau comportement: Delta ne s'applique pas aux variables liées par un let	herbelin	2002-03-01
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	GROS COMMIT:	barras	2001-11-05
*	Suppression des arguments sur les constantes, inductifs et constructeurs	barras	2001-10-09
*	Transparent	barras	2001-09-20
*	Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...	herbelin	2001-07-21
*	Nettoyage/restructuration des ensembles d'indicateurs de réductions	herbelin	2001-07-02
*	Changement de la structure des points fixes	barras	2001-05-03
*	entetes	filliatr	2001-03-15
*	nouvelle implantation de la reduction	barras	2001-03-01