coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	ajout decimal_exp pour interpreter les notations decimales	mohring	2004-03-12
*	ide: silent behavior better, save icon, -byte works	marche	2004-03-03
*	MAJ Commentaires	herbelin	2004-02-28
*	Ajout delimiteur pour bool_scope	herbelin	2004-02-12
*	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin	2004-02-12
*	backtrack implicit dans Bvector	marche	2004-02-10
*	patch Bvector: args implicites	marche	2004-02-09
*	MAJ simplification	herbelin	2004-01-27
*	Suppression de Rsyntax en v8	herbelin	2004-01-13
*	bugs avec Pose et Assert	barras	2004-01-09
*	Commentaires en v8	herbelin	2004-01-09
*	Ajout delimiteur et arguments de scope pour list	herbelin	2003-12-24
*	changement de pose en set (pose n'etait pas utilise avec la semantique	barras	2003-12-24
*	Finalement, espacement autour du ':' pour a la fois exists, forall et fun	herbelin	2003-12-23
*	Affichage sur le modèle du forall pour le exists	herbelin	2003-12-21
*	Duplication temporaire des règles de syntaxe des paires	herbelin	2003-12-16
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	power associe a droite	marche	2003-12-05
*	Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...	herbelin	2003-12-04
*	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
*	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-29
*	Protection contre les renommages; redondances	herbelin	2003-11-28
*	Renoncement de la compatibilite des noms qualifies au profit de la compatibil...	herbelin	2003-11-24
*	Compatibilite	herbelin	2003-11-22
*	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-21
*	ajout de Znumtheory.v dans ZArith	letouzey	2003-11-19
*	Restauration compatibilite 7.4 pour le Hint Unfold Rgt	herbelin	2003-11-19
*	Un nouveau lemme redondant ...	herbelin	2003-11-18
*	Deplacement ZERO_le_inj dans Zorder	herbelin	2003-11-18
*	Meilleure solution pour la compatibilite	herbelin	2003-11-15
*	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-14
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras	2003-11-13