coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	Ratage standardisation Rge_monotony en Rmult_ge_compat_r	herbelin	2003-12-01
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Ajout lemmes, simplification preuve de SeqProp	herbelin	2003-11-29
*	Protection contre les renommages; redondances	herbelin	2003-11-28
*	Restauration compatibilite 7.4 pour le Hint Unfold Rgt	herbelin	2003-11-19
*	Meilleure solution pour la compatibilite	herbelin	2003-11-15
*	MAJ INZ	herbelin	2003-11-12
*	Restauration preference Rge a Rle pour compatibilite...; petit nettoyage	herbelin	2003-11-02
*	lettac -> set	barras	2003-10-16
*	Ajout de quelques lemmes cles	herbelin	2003-10-16
*	INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...	herbelin	2003-06-12
*	"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Reals	herbelin	2003-05-24
*	En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...	herbelin	2003-04-29
*	Open Scope en Local	herbelin	2003-04-12
*	Remplacement Import par Open Scope en v8	herbelin	2003-04-10
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".	herbelin	2003-04-09
*	Ajout Implicit Variable Type	herbelin	2003-03-31
*	* empty log message *	barras	2003-03-21
*	* empty log message *	barras	2003-03-12
*	Restructuration des hints pour qu'Auto fasse moins de détours et les	herbelin	2003-02-27
*	Suppression de INR2 / Conséquence logique de la nouvelle représentation des...	desmettr	2003-01-21
*	Renommage de Rbase.v en RIneq.v	desmettr	2003-01-16