coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin	2003-11-24
*	Renoncement de la compatibilite des noms qualifies au profit de la compatibil...	herbelin	2003-11-24
*	maj	filliatr	2003-11-24
*	maj	filliatr	2003-11-24
*	MAJ	herbelin	2003-11-23
*	MAJs	herbelin	2003-11-23
*	Prise en compte des definitions locales dans les (co-)points-fixes	herbelin	2003-11-23
*	Compatibilite	herbelin	2003-11-22
*	Traitement plus clair, notamment pour Locate, de quand quoter les composantes...	herbelin	2003-11-22
*	Bug introduit avec le 'Simpl f'	herbelin	2003-11-22
*	maj	filliatr	2003-11-22
*	maj	filliatr	2003-11-22
*	Suppression des niveaux vides	herbelin	2003-11-21
*	ajout Pnat et Pcompare_antisym	herbelin	2003-11-21
*	Ajout 'Simpl f'	herbelin	2003-11-21
*	Simplification; ajout Zcompare_antisym	herbelin	2003-11-21
*	ajout Pnat (suite)	herbelin	2003-11-21
*	ajout Pnat (suite)	herbelin	2003-11-21
*	Extraction des lemmes sur convert/nat_of_P de BinPos vers Pnat; ajout Pcase e...	herbelin	2003-11-21
*	Ajout Print Implicit	herbelin	2003-11-21
*	Tri et typo	herbelin	2003-11-21
*	MAJ format et doc	herbelin	2003-11-21
*	Pas d'entrees autres que les predefinies en v8	herbelin	2003-11-21
*	maj	filliatr	2003-11-21
*	Nouvelle solution pour le probleme d'effacement des niveaux vides de opercons...	herbelin	2003-11-20
*	Code simplification in CC	corbinea	2003-11-20
*	maj	filliatr	2003-11-20
*	maj	filliatr	2003-11-20
*	ajout de Znumtheory.v dans ZArith	letouzey	2003-11-19
*	Restauration compatibilite 7.4 pour le Hint Unfold Rgt	herbelin	2003-11-19
*	Prise en compte renommages	herbelin	2003-11-19
*	Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...	herbelin	2003-11-19
*	Deplacement subst_rawconstr dans Rawterm	herbelin	2003-11-19
*	Protection contre l'effacement des niveaux vides de operconstr et pattern par...	herbelin	2003-11-19
*	maj	filliatr	2003-11-19
*	correction suite ajout nouvelles tactiques	clrenard	2003-11-18
*	reparation bug moins unaire (erreur de PP)	barras	2003-11-18
*	.v8	herbelin	2003-11-18
*	tout clean-ide dans clean	herbelin	2003-11-18
*	MAJ	herbelin	2003-11-18
*	Bug: faut brancher la sortie des tactiques sur stdout pendant traduction	herbelin	2003-11-18
*	Mise en place systeme de qualification des noms renommes; Renommages dans Rin...	herbelin	2003-11-18
*	Code mort	herbelin	2003-11-18
*	Blindage vis a vis des constructeurs partiellement appliques	herbelin	2003-11-18
*	Ajout mis_constructor_nargs_env	herbelin	2003-11-18
*	Ajout recarg_length	herbelin	2003-11-18
*	Un nouveau lemme redondant ...	herbelin	2003-11-18
*	Deplacement ZERO_le_inj dans Zorder	herbelin	2003-11-18
*	Utilisation de la date cvs dans l'en-tete si make.result existe	herbelin	2003-11-18
*	* empty log message *	filliatr	2003-11-18