coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...	herbelin	2003-04-29
*	Un principe light d'elimination de Acc, suivant les remarques de Yves Bertot	letouzey	2003-04-28
*	Intégration DatatypesSyntax à Datatypes	herbelin	2003-04-17
*	Divers	herbelin	2003-04-17
*	<> maintenant standard	herbelin	2003-04-17
*	Intégration DatatypesSyntax à Datatypes	herbelin	2003-04-17
*	Syntaxe 'x=y:>T'	herbelin	2003-04-17
*	suite au commit d'hugo dans TypeSyntax & Raxiom, Intro donnait un nom different	letouzey	2003-04-16
*	sumboolT, sumorT, sigTT, SigT redondants	herbelin	2003-04-16
*	Cosmetique	herbelin	2003-04-14
*	Local 'o'	herbelin	2003-04-14
*	Open Scope en Local	herbelin	2003-04-12
*	Open Scope remplace Import	herbelin	2003-04-10
*	Calcul automatique de l'implicite de nil pour que l'affichage sache le traiter	herbelin	2003-04-10
*	Remplacement Import par Open Scope en v8	herbelin	2003-04-10
*	cast de nil	herbelin	2003-04-09
*	nil en implicite dans la v8	herbelin	2003-04-09
*	Ajout Open Scope	herbelin	2003-04-09
*	Activation des implicites pour la v8	herbelin	2003-04-09
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
*	Renommage K; equivalence JMeq et eq_dep sur Type	herbelin	2003-04-09
*	Defined	herbelin	2003-04-09
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".	herbelin	2003-04-09
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
*	Nommage explicite des hypotheses introduites quand le nom existe aussi comme ...	herbelin	2003-04-07
*	Cosmetique	herbelin	2003-04-07
*	Espaces superflus	herbelin	2003-04-07
*	Documentation, généralisation à eq sur Type, preuves d'équivalence des	herbelin	2003-04-03
*	Ajout double_plus	herbelin	2003-03-31
*	Ajout Implicit Variable Type	herbelin	2003-03-31
*	Suppression des alias eqT/exT/exT2 en nouvelle syntaxe	herbelin	2003-03-31
*	Notation eqT superflue	herbelin	2003-03-31
*	eq fusionne avec eqT et devient par défaut sur Type,	herbelin	2003-03-29
*	Déplacement de minus dans Peano	herbelin	2003-03-29
*	Implicit Variables Type	herbelin	2003-03-29
*	Pas d'associativité gauche au niveau 3 en vieille syntaxe !	herbelin	2003-03-28
*	notations <>, Assumption avec existentiel, replace term	mohring	2003-03-28
*	* empty log message *	barras	2003-03-21
*	* empty log message *	barras	2003-03-14
*	* empty log message *	barras	2003-03-12
*	Restructuration des hints pour qu'Auto fasse moins de détours et les	herbelin	2003-02-27
*	Ajout du theoreme de Cesaro	desmettr	2003-02-14
*	Modifications dans une tactique toplevel	delahaye	2003-02-13
*	Pb de parenthèse dans "Check (S (plus O O))"	herbelin	2003-01-30
*	MAJ pour Reg	desmettr	2003-01-28
*	Documentation du contenu de REALS	desmettr	2003-01-22
*	Modifications dans SeqProp	desmettr	2003-01-22
*	Renommages dans Rtrigo_def	desmettr	2003-01-22
*	Commentaires	desmettr	2003-01-22
*	Renommages nombreux	desmettr	2003-01-22