coq - The formal proof system

Age	Commit message (Expand)	Author
2008-03-08	Fix bugs that were reopened due to the change of setoid	msozeau
2008-03-07	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey
2008-03-06	Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?n	herbelin
2008-03-05	Correction d'une typo restant du commit 10557 et cause d'échec de contribs	herbelin
2008-02-21	congruence now knows about _ -> _	corbinea
2008-02-19	added products and sorts as possible heads for canonical structures	corbinea
2008-02-14	Added default canonical structures (see example in test-suite)	corbinea
2008-02-11	Correction d'un bug de clear	notin
2008-02-06	Correction d'un bug à l'interprétation de "change" (on exigeait que	herbelin
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-23	Ajout d'un test pour le mode déclaratif + test pour le bug #1776	notin
2008-01-02	Better resolution of implicit parameters in typeclass binders, add extensiona...	msozeau
2007-09-26	Complément aux commits 10124 et 10125 sur l'inférence de type (correction	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-08-25	Extension et documentation de real_clean/evar_define dans evarutil.ml:	herbelin
2007-08-10	Ajout d'un exemple d'inversion des dépendances dans le prédicat comme	herbelin
2007-08-08	Add a test case for the new "dependent" induction tactics.	msozeau
2007-07-18	A generic preprocessing tactic zify for (r)omega	letouzey
2007-07-09	Improvements / Bug fixes for ROmega	letouzey
2007-05-28	Contrôle de la compatibilité de apply via une information dans les	herbelin
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-04-30	Modification syntaxe de Test	herbelin
2007-04-29	Correction bug #1507 (report révision 9807 de v8.1 vers trunk)	herbelin
2007-04-13	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-03-15	Test de non-régression pour commit 9673	herbelin
2007-02-21	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-15	Réparation absence d'interprétation des liaisons vers listes	herbelin
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-02-01	Report de la révision 9577 dans le trunk	notin
2007-01-25	Redondance erronée dans les tests	herbelin
2007-01-22	Correction d'un bug d'unification-pattern dans l'algo d'unification	herbelin
2007-01-22	Correction pour le rapport de bug #1325 par rétablissement du	herbelin
2007-01-12	Suite au mail de Lionel a propos du Makefile:	letouzey
2006-12-13	Alignement de la politique de renommage de rename_bound_var (utilisé pour	herbelin
2006-12-13	Dépliage du terme d'induction avant suppression quand celui-ci est un	herbelin
2006-12-12	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin
2006-11-19	Raffinement de l'unification de "apply": mémorisation de certains	herbelin
2006-11-13	Correction typo	herbelin
2006-11-10	Ajout de dépliage de l'énoncé, si besoin est, dans apply in	herbelin
2006-11-10	Correction d'un bug refine	herbelin