coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	ajout decimal_exp pour interpreter les notations decimales	mohring	2004-03-12
*	Suppression de Rsyntax en v8	herbelin	2004-01-13
*	bugs avec Pose et Assert	barras	2004-01-09
*	changement de pose en set (pose n'etait pas utilise avec la semantique	barras	2003-12-24
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	power associe a droite	marche	2003-12-05
*	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
*	Utilisation du total_order non constructif	herbelin	2003-11-29
*	Protection contre les renommages; redondances	herbelin	2003-11-28
*	Restauration compatibilite 7.4 pour le Hint Unfold Rgt	herbelin	2003-11-19
*	Meilleure solution pour la compatibilite	herbelin	2003-11-15
*	MAJ INZ	herbelin	2003-11-12
*	Restauration preference Rge a Rle pour compatibilite...	herbelin	2003-11-02
*	Restauration preference Rge a Rle pour compatibilite...; petit nettoyage	herbelin	2003-11-02
*	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...	herbelin	2003-10-30
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	R passe dans Set !	herbelin	2003-10-20
*	20 est uniquement associatif a gauche	herbelin	2003-10-17
*	lettac -> set	barras	2003-10-16
*	Pour eviter des regles redondantes en v7	herbelin	2003-10-16
*	FTC_P2 maintenant dans RIneq	herbelin	2003-10-16
*	Ajout de quelques lemmes cles	herbelin	2003-10-16
*	Affichage = au lieu de == en v7	herbelin	2003-10-15
*	Notations pour l'exponentiation	herbelin	2003-10-13
*	Notation '^'	herbelin	2003-10-10
*	Cacher les .v8	herbelin	2003-10-03
*	Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...	herbelin	2003-09-23
*	Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...	herbelin	2003-09-21
*	Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...	herbelin	2003-09-19
*	Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...	herbelin	2003-09-19
*	Ajout et MAJ commandes de scopes	herbelin	2003-09-12
*	Bind et Delimit pour R	herbelin	2003-09-12
*	Bind et Delimit pour R	herbelin	2003-09-12
*	INZ reste constante pour compat V7 mais Unfold INZ est supprimé par le tradu...	herbelin	2003-06-12
*	niveau 49 devient next	herbelin	2003-05-29
*	"INZ" déplacé en V8 dans ZArith, juste syntaxique en V7 dans Reals	herbelin	2003-05-24
*	Bug	herbelin	2003-05-21
*	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
*	En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...	herbelin	2003-04-29
*	Divers	herbelin	2003-04-17
*	<> maintenant standard	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