aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2008-04-03Chgts mineurs:herbelin
2008-04-02Minor fixes. Use expanded type in class_tactics for Morphism search, tomsozeau
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-03-29Fix test-suite files, change conflicting notation "->rel" and the othersmsozeau
2008-03-28Improve error handling and messages for typeclasses. msozeau
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-03-26Diverses petites modifs dans la test-suite:notin
2008-03-16Misc: Add test for bug 1704, now closed. Add usual syntax for lists inmsozeau
2008-03-15Forgot the test file.msozeau
2008-03-15Backtrack sur le test censé discriminer entre une erreur d'evar nonherbelin
2008-03-10Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)herbelin
2008-03-08New implementation of Add Relation as a DefaultRelation instancemsozeau
2008-03-08Fix bugs that were reopened due to the change of setoidmsozeau
2008-03-07f_equal, revert, specialize in ML, contradict in better Ltac (+doc)letouzey
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-11Correction d'un bug de clearnotin
2008-02-06Correction d'un bug à l'interprétation de "change" (on exigeait queherbelin
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-23Ajout d'un test pour le mode déclaratif + test pour le bug #1776notin
2008-01-02Better resolution of implicit parameters in typeclass binders, add extensiona...msozeau
2007-09-26Complément aux commits 10124 et 10125 sur l'inférence de type (correction herbelin
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-08-25Extension et documentation de real_clean/evar_define dans evarutil.ml:herbelin
2007-08-10Ajout d'un exemple d'inversion des dépendances dans le prédicat commeherbelin
2007-08-08Add a test case for the new "dependent" induction tactics.msozeau
2007-07-18A generic preprocessing tactic zify for (r)omegaletouzey
2007-07-09Improvements / Bug fixes for ROmega letouzey
2007-05-28Contrôle de la compatibilité de apply via une information dans lesherbelin
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-04-30Modification syntaxe de Testherbelin
2007-04-29Correction bug #1507 (report révision 9807 de v8.1 vers trunk)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-03-15Test de non-régression pour commit 9673herbelin
2007-02-21Correction typo liée au commit 8779 (levait une anomalie)herbelin
2007-02-21Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESherbelin
2007-02-15Réparation absence d'interprétation des liaisons vers listesherbelin
2007-02-13Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deherbelin