coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Ajouts de quelques tests sur les bugs	notin	2007-12-21
*	Ajout d'un test pour le bug #1100	notin	2007-12-12
*	Test pour le bug #1754	notin	2007-12-11
*	Quelques exemples à méditer sur le polymorphisme d'universe des inductifs	herbelin	2007-10-24
*	Vérification que "rewrite in" se comporte comme "rewrite" et échoue	herbelin	2007-10-16
*	Correction de quelques défauts d'affichage (notations sous "as" pour	herbelin	2007-10-05
*	Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)	herbelin	2007-10-04
*	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin	2007-09-26
*	Correction d'un bug dans check + ajout de tests	notin	2007-09-21
*	- Fixing bug 1703 ("intros until n" falls back on the variable name when	herbelin	2007-09-21
*	Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)	herbelin	2007-09-18
*	Raffinement de l'algorithme d'inférence de type	herbelin	2007-09-17
*	Réponse à une incompatibilité introduite dans 10114 (calcul du nombre	herbelin	2007-09-16
*	Correction du bug #1679 (congruence) et ajout test-suite	corbinea	2007-09-14
*	Itération sur les sous-termes dans la vérification de la condition de garde	herbelin	2007-09-06
*	Extension et documentation de real_clean/evar_define dans evarutil.ml:	herbelin	2007-08-25
*	Correction du bug #1634 + ajout de bugs dans la test-suite	notin	2007-08-22
*	Correction du bug #1322	notin	2007-08-16
*	Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;	notin	2007-08-16
*	Ajout d'un exemple d'inversion des dépendances dans le prédicat comme	herbelin	2007-08-10
*	Typo	notin	2007-08-10
*	Modification de la test suite pour intégrer des tests spécifiques aux	notin	2007-08-10
*	Add a test case for the new "dependent" induction tactics.	msozeau	2007-08-08
*	removed thesis	barras	2007-07-23
*	A generic preprocessing tactic zify for (r)omega	letouzey	2007-07-18
*	Update (test-suite was not successful).	glondu	2007-07-12
*	Improvements / Bug fixes for ROmega	letouzey	2007-07-09
*	Factorisation des paramètres dans l'affichage des inductifs	herbelin	2007-07-02
*	Contrôle de la compatibilité de apply via une information dans les	herbelin	2007-05-28
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9859 85f007b7-540e-04...	soubiran	2007-05-25
*	Unification suite: petits affinements pour préserver la compatibilité	herbelin	2007-05-24
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	Wish #1582 (3eme)	herbelin	2007-05-18
*	Correction bug calcul des implicites en présence d'evars dans les types	herbelin	2007-05-16
*	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin	2007-05-10
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06
*	Modification syntaxe de Test	herbelin	2007-04-30
*	Correction bug #1507 (report révision 9807 de v8.1 vers trunk)	herbelin	2007-04-29
*	Ajout d'un test de complexité de injection (cf bug 1173)	herbelin	2007-04-14
*	Correction bug #1477 sur ordre des variables partagées par les or-patterns.	herbelin	2007-04-13
*	Test non régression bug #1491	herbelin	2007-04-13
*	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin	2007-04-13
*	Un chouia de portabilité en plus et pas de test si pas de bogomips	herbelin	2007-03-19
*	MAJ test complexité pour considérer le cas d'un temps avec un nombre	herbelin	2007-03-17
*	Test de non-régression pour commit 9673	herbelin	2007-03-15
*	Correction typo liée au commit 8779 (levait une anomalie)	herbelin	2007-02-21
*	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin	2007-02-21
*	Removed some useless code in mod_typing that was redundant with safe_typing.	soubiran	2007-02-21
*	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran	2007-02-21