aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2008-03-06Plug the new setoid implemtation in, leaving the original one commentedmsozeau
2008-03-06Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?nherbelin
2008-03-05Correction d'une typo restant du commit 10557 et cause d'échec de contribsherbelin
2008-02-21congruence now knows about _ -> _corbinea
2008-02-19added products and sorts as possible heads for canonical structurescorbinea
2008-02-14Added default canonical structures (see example in test-suite)corbinea
2008-02-14Backtrack changes on eauto, move specialized version of eauto inmsozeau
2008-02-11Correction d'un bug de clearnotin
2008-02-08Backport code from command.ml to subtac_command.ml for defininingmsozeau
2008-02-06Correction d'un bug à l'interprétation de "change" (on exigeait queherbelin
2008-02-05Ajout d'un test pour le bug #1787notin
2008-02-01Ajout de 2 testsnotin
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2008-02-01Unification de TacLetRecIn et TacLetIn. En particulier, on peutherbelin
2008-01-31Debug implementation of dependent induction/dependent destruction and documen...msozeau
2008-01-30Work on dependent induction tactic and friends, finish the test-suite examplemsozeau
2008-01-24Fermeture du bug #1754notin
2008-01-23Ajout d'un test pour le bug #1779notin
2008-01-23Ajout d'un test pour le mode déclaratif + test pour le bug #1776notin
2008-01-22Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)notin
2008-01-21Correction du bug #1754notin
2008-01-02Better resolution of implicit parameters in typeclass binders, add extensiona...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-21Ajouts de quelques tests sur les bugsnotin
2007-12-12Ajout d'un test pour le bug #1100notin
2007-12-11Test pour le bug #1754notin
2007-10-24Quelques exemples à méditer sur le polymorphisme d'universe des inductifsherbelin
2007-10-16Vérification que "rewrite in" se comporte comme "rewrite" et échoueherbelin
2007-10-05Correction de quelques défauts d'affichage (notations sous "as" pourherbelin
2007-10-04Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)herbelin
2007-09-26Complément aux commits 10124 et 10125 sur l'inférence de type (correction herbelin
2007-09-21Correction d'un bug dans check + ajout de testsnotin
2007-09-21- Fixing bug 1703 ("intros until n" falls back on the variable name whenherbelin
2007-09-18Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)herbelin
2007-09-17Raffinement de l'algorithme d'inférence de typeherbelin
2007-09-16Réponse à une incompatibilité introduite dans 10114 (calcul du nombreherbelin
2007-09-14Correction du bug #1679 (congruence) et ajout test-suitecorbinea
2007-09-06Itération sur les sous-termes dans la vérification de la condition de gardeherbelin
2007-08-25Extension et documentation de real_clean/evar_define dans evarutil.ml:herbelin
2007-08-22Correction du bug #1634 + ajout de bugs dans la test-suitenotin
2007-08-16Correction du bug #1322notin
2007-08-16Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;notin
2007-08-10Ajout d'un exemple d'inversion des dépendances dans le prédicat commeherbelin
2007-08-10Typonotin
2007-08-10Modification de la test suite pour intégrer des tests spécifiques auxnotin
2007-08-08Add a test case for the new "dependent" induction tactics.msozeau
2007-07-23removed thesisbarras
2007-07-18A generic preprocessing tactic zify for (r)omegaletouzey
2007-07-12Update (test-suite was not successful).glondu
2007-07-09Improvements / Bug fixes for ROmega letouzey