coq - The formal proof system

Age	Commit message (Expand)	Author
2008-02-08	Backport code from command.ml to subtac_command.ml for definining	msozeau
2008-02-06	Correction d'un bug à l'interprétation de "change" (on exigeait que	herbelin
2008-02-05	Ajout d'un test pour le bug #1787	notin
2008-02-01	Ajout de 2 tests	notin
2008-02-01	Beaoucoup de changements dans la representation interne des modules.	soubiran
2008-02-01	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin
2008-01-31	Debug implementation of dependent induction/dependent destruction and documen...	msozeau
2008-01-30	Work on dependent induction tactic and friends, finish the test-suite example	msozeau
2008-01-24	Fermeture du bug #1754	notin
2008-01-23	Ajout d'un test pour le bug #1779	notin
2008-01-23	Ajout d'un test pour le mode déclaratif + test pour le bug #1776	notin
2008-01-22	Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)	notin
2008-01-21	Correction du bug #1754	notin
2008-01-02	Better resolution of implicit parameters in typeclass binders, add extensiona...	msozeau
2007-12-31	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau
2007-12-21	Ajouts de quelques tests sur les bugs	notin
2007-12-12	Ajout d'un test pour le bug #1100	notin
2007-12-11	Test pour le bug #1754	notin
2007-10-24	Quelques exemples à méditer sur le polymorphisme d'universe des inductifs	herbelin
2007-10-16	Vérification que "rewrite in" se comporte comme "rewrite" et échoue	herbelin
2007-10-05	Correction de quelques défauts d'affichage (notations sous "as" pour	herbelin
2007-10-04	Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)	herbelin
2007-09-26	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	herbelin
2007-09-21	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-18	Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)	herbelin
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-09-16	Réponse à une incompatibilité introduite dans 10114 (calcul du nombre	herbelin
2007-09-14	Correction du bug #1679 (congruence) et ajout test-suite	corbinea
2007-09-06	Itération sur les sous-termes dans la vérification de la condition de garde	herbelin
2007-08-25	Extension et documentation de real_clean/evar_define dans evarutil.ml:	herbelin
2007-08-22	Correction du bug #1634 + ajout de bugs dans la test-suite	notin
2007-08-16	Correction du bug #1322	notin
2007-08-16	Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;	notin
2007-08-10	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-08	Add a test case for the new "dependent" induction tactics.	msozeau
2007-07-23	removed thesis	barras
2007-07-18	A generic preprocessing tactic zify for (r)omega	letouzey
2007-07-12	Update (test-suite was not successful).	glondu
2007-07-09	Improvements / Bug fixes for ROmega	letouzey
2007-07-02	Factorisation des paramètres dans l'affichage des inductifs	herbelin
2007-05-28	Contrôle de la compatibilité de apply via une information dans les	herbelin
2007-05-25	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9859 85f007b7-540e-04...	soubiran
2007-05-24	Unification suite: petits affinements pour préserver la compatibilité	herbelin
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-18	Wish #1582 (3eme)	herbelin
2007-05-16	Correction bug calcul des implicites en présence d'evars dans les types	herbelin
2007-05-10	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin