coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Amelioration presentation	herbelin	2003-05-14
*	Amelioration affichage	herbelin	2003-05-14
*	Suppression de 'R' dans la notation == entre	herbelin	2003-05-14
*	Suppression de 'R' dans la notation == entre	herbelin	2003-05-14
*	Deplacement lemmes sur fact de Reals vers Arith	herbelin	2003-05-14
*	Nouveaux lemmes	herbelin	2003-05-13
*	Nouveaux lemmes (sur proposition de Nijmegen)	herbelin	2003-05-13
*	Nouveaux lemmes (sur proposition de Nijmegen)	herbelin	2003-05-13
*	ajout inverse relation bien fondee	mohring	2003-05-09
*	coqide: toolbar/autosave	monate	2003-05-07
*	Blancs	herbelin	2003-04-29
*	Notations	herbelin	2003-04-29
*	Implicit Types	herbelin	2003-04-29
*	Ajout ChoiceFacts	herbelin	2003-04-29
*	Blancs	herbelin	2003-04-29
*	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