coq - The formal proof system

Age	Commit message (Expand)	Author
2003-05-22	Ajout V8Notation	herbelin
2003-05-21	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin
2003-05-21	Notations	herbelin
2003-05-21	Bug	herbelin
2003-05-14	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-13	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-09	ajout inverse relation bien fondee	mohring
2003-05-07	coqide: toolbar/autosave	monate
2003-04-29	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-28	Un principe light d'elimination de Acc, suivant les remarques de Yves Bertot	letouzey
2003-04-17	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-16	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-14	Cosmetique	herbelin
2003-04-14	Local 'o'	herbelin
2003-04-12	Open Scope en Local	herbelin
2003-04-10	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-09	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-07	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-03	Documentation, généralisation à eq sur Type, preuves d'équivalence des	herbelin
2003-03-31	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