coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Transparency of Z_lt_le_dec	notin	2007-04-12
*	Bug nommage Zgt_trans_succ	herbelin	2006-12-12
*	correction Open Local Scope (Ring)	bgregoir	2006-12-11
*	Changement dans le kernel :	bgregoir	2006-12-11
*	fixed field_simplify + changed precedence of let and fun in ltac	barras	2006-10-30
*	simplif de la partie ML de ring/field	barras	2006-10-27
*	Mise en forme des theories	notin	2006-10-17
*	revert, the previous commit was a mistake	bertot	2006-10-05
*	A version of natprering that should be more efficient and removal of a bad	bertot	2006-10-05
*	Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom	barras	2006-10-05
*	commit de field + renommages	barras	2006-09-26
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
*	Ajout de Zgcd_spec (compat.)	notin	2006-06-26
*	nouvel algorithme pour Zgcd (plus rapide) + un Qcompare	letouzey	2006-06-25
*	Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...	herbelin	2006-06-09
*	ajout de QArith dans les theories standards	letouzey	2006-05-31
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
*	Changement de prÃ©cÃ©dence de l'argument du by de assert; consÃ©quences...	herbelin	2006-05-23
*	On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_pos	letouzey	2006-05-14
*	typo	letouzey	2006-05-13
*	un Zgcd calculant dans coq	letouzey	2006-05-13
*	une fonction pouvant calculer le gcd en coq	letouzey	2006-05-11
*	un Zgcd general gardant trace des coefs	letouzey	2006-05-05
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin	2006-04-28
*	Bug Scope	herbelin	2006-02-12
*	Nettoyage Zmin.v, création Zmax.v et Zminmax.v	herbelin	2006-02-12
*	Finalement, préservation de la compatibilité pour Z_lt_induction et ajout p...	herbelin	2005-05-02
*	Lemme de passage de l'autre côté d'une égalité	herbelin	2005-05-02
*	Fixed hypotheses of Z_lt_induction (see #957)	herbelin	2005-04-26
*	Missing translating a 'O' into a '0' (again - cf bug #947); removed useless h...	herbelin	2005-03-29
*	Missing translating a 'O' into a '0'	herbelin	2005-03-24
*	Changement dans les boxed values .	gregoire	2004-11-12
*	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin	2004-10-11
*	Zbool déjà dans ZArith_base	herbelin	2004-08-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	backtrack implicit dans Bvector	marche	2004-02-10
*	patch Bvector: args implicites	marche	2004-02-09
*	changement de pose en set (pose n'etait pas utilise avec la semantique	barras	2003-12-24
*	Duplication temporaire des règles de syntaxe des paires	herbelin	2003-12-16
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...	herbelin	2003-12-04
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	ground->firstorder, cc-> congruence, CC final commit	corbinea	2003-11-29
*	Report de lemmes de Znumtheory dans Zabs ou BinInt	herbelin	2003-11-29
*	Renoncement de la compatibilite des noms qualifies au profit de la compatibil...	herbelin	2003-11-24
*	Compatibilite	herbelin	2003-11-22
*	Simplification; ajout Zcompare_antisym	herbelin	2003-11-21
*	ajout Pnat (suite)	herbelin	2003-11-21
*	ajout de Znumtheory.v dans ZArith	letouzey	2003-11-19
*	Un nouveau lemme redondant ...	herbelin	2003-11-18