aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2007-07-02Factorisation des paramètres dans l'affichage des inductifsherbelin
2007-05-28Contrôle de la compatibilité de apply via une information dans lesherbelin
2007-05-25git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9859 85f007b7-540e-04...soubiran
2007-05-24Unification suite: petits affinements pour préserver la compatibilitéherbelin
2007-05-22Nouvelle stratégie d'unification des types des with-bindings dansherbelin
2007-05-18Wish #1582 (3eme)herbelin
2007-05-16Correction bug calcul des implicites en présence d'evars dans les typesherbelin
2007-05-10Prise en compte réversibilité des notations de la forme "Notation Nil := @n...herbelin
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
2007-04-30Modification syntaxe de Testherbelin
2007-04-29Correction bug #1507 (report révision 9807 de v8.1 vers trunk)herbelin
2007-04-14Ajout d'un test de complexité de injection (cf bug 1173)herbelin
2007-04-13Correction bug #1477 sur ordre des variables partagées par les or-patterns.herbelin
2007-04-13Test non régression bug #1491herbelin
2007-04-13Nettoyage des tactiques basées sur "simpl" (delta-réduction cachantherbelin
2007-03-19Un chouia de portabilité en plus et pas de test si pas de bogomipsherbelin
2007-03-17MAJ test complexité pour considérer le cas d'un temps avec un nombreherbelin
2007-03-15Test de non-régression pour commit 9673herbelin
2007-02-21Correction typo liée au commit 8779 (levait une anomalie)herbelin