coq - The formal proof system

Age	Commit message (Expand)	Author
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2003-11-29	Notation locale pour Rpower	herbelin
2003-11-29	Ajout lemmes, simplification preuve de SeqProp	herbelin
2003-11-29	ground->firstorder, cc-> congruence, CC final commit	corbinea
2003-11-29	Utilisation du total_order non constructif	herbelin
2003-11-29	Report de lemmes de Znumtheory dans Zabs ou BinInt	herbelin
2003-11-28	Protection contre les renommages; redondances	herbelin
2003-11-24	Renoncement de la compatibilite des noms qualifies au profit de la compatibil...	herbelin
2003-11-22	Compatibilite	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	Tri et typo	herbelin
2003-11-19	ajout de Znumtheory.v dans ZArith	letouzey
2003-11-19	Restauration compatibilite 7.4 pour le Hint Unfold Rgt	herbelin
2003-11-18	Un nouveau lemme redondant ...	herbelin
2003-11-18	Deplacement ZERO_le_inj dans Zorder	herbelin
2003-11-15	Meilleure solution pour la compatibilite	herbelin
2003-11-14	Pour les .v8	herbelin
2003-11-14	Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_base	herbelin
2003-11-14	cosmetique	herbelin
2003-11-14	Presentation	herbelin
2003-11-14	Ordre standard pour l'associativite	herbelin
2003-11-14	Quelques oublis pour que les notations marchent bien	herbelin
2003-11-14	Bug implicit arguments	herbelin
2003-11-14	Automatisation de la traduction de iff_trans; renommage IF	herbelin
2003-11-14	Backtrack sur Peano	herbelin
2003-11-14	Nouveaux lemmes 'canoniques'; compatibilite	herbelin
2003-11-13	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras
2003-11-13	Oubli report Nul/Pos	herbelin
2003-11-13	Require	herbelin
2003-11-13	qq petit ajouts à Zdiv	letouzey
2003-11-12	MAJ INZ	herbelin
2003-11-12	Ajout lemme projections	herbelin
2003-11-12	%type au lieu de %T	herbelin
2003-11-12	Lemmes dans un sens plus naturel	herbelin
2003-11-12	Restructuration ZArith	herbelin
2003-11-12	Cosmetique	herbelin
2003-11-12	Noms canoniques pour les variables liees	herbelin
2003-11-12	Independance vis a vis noms variables liees; partie sur bool dans Zbool	herbelin
2003-11-12	Noms/énoncés plus canoniques	herbelin
2003-11-12	Independance vis a vis noms variables liees	herbelin
2003-11-12	Ajout lemmes; independance vis a vis noms variables liees; restructuration	herbelin
2003-11-12	Ajout partie sur bool anciennement dans Zmisc	herbelin
2003-11-12	Ajout lemmes; independance vis a vis noms variables liees	herbelin
2003-11-12	On sait jamais	herbelin
2003-11-12	petits changements de syntaxe	barras
2003-11-09	Ajout quelques lemmes; noms des variables liees	herbelin
2003-11-07	Oubli BinNat	herbelin