aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
* New implementation of Add Relation as a DefaultRelation instanceGravatar msozeau2008-03-08
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?nGravatar herbelin2008-03-06
* Correction d'une typo restant du commit 10557 et cause d'échec de contribsGravatar herbelin2008-03-05
* congruence now knows about _ -> _Gravatar corbinea2008-02-21
* added products and sorts as possible heads for canonical structuresGravatar corbinea2008-02-19
* Added default canonical structures (see example in test-suite)Gravatar corbinea2008-02-14
* Backtrack changes on eauto, move specialized version of eauto inGravatar msozeau2008-02-14
* Correction d'un bug de clearGravatar notin2008-02-11
* Backport code from command.ml to subtac_command.ml for defininingGravatar msozeau2008-02-08
* Correction d'un bug à l'interprétation de "change" (on exigeait queGravatar herbelin2008-02-06
* Ajout d'un test pour le bug #1787Gravatar notin2008-02-05
* Ajout de 2 testsGravatar notin2008-02-01
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Debug implementation of dependent induction/dependent destruction and documen...Gravatar msozeau2008-01-31
* Work on dependent induction tactic and friends, finish the test-suite exampleGravatar msozeau2008-01-30
* Fermeture du bug #1754Gravatar notin2008-01-24
* Ajout d'un test pour le bug #1779Gravatar notin2008-01-23
* Ajout d'un test pour le mode déclaratif + test pour le bug #1776Gravatar notin2008-01-23
* Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)Gravatar notin2008-01-22
* Correction du bug #1754Gravatar notin2008-01-21
* Better resolution of implicit parameters in typeclass binders, add extensiona...Gravatar msozeau2008-01-02
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Ajouts de quelques tests sur les bugsGravatar notin2007-12-21
* Ajout d'un test pour le bug #1100Gravatar notin2007-12-12
* Test pour le bug #1754Gravatar notin2007-12-11
* Quelques exemples à méditer sur le polymorphisme d'universe des inductifsGravatar herbelin2007-10-24
* Vérification que "rewrite in" se comporte comme "rewrite" et échoueGravatar herbelin2007-10-16
* Correction de quelques défauts d'affichage (notations sous "as" pourGravatar herbelin2007-10-05
* Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)Gravatar herbelin2007-10-04
* Complément aux commits 10124 et 10125 sur l'inférence de type (correction Gravatar herbelin2007-09-26
* Correction d'un bug dans check + ajout de testsGravatar notin2007-09-21
* - Fixing bug 1703 ("intros until n" falls back on the variable name whenGravatar herbelin2007-09-21
* Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)Gravatar herbelin2007-09-18
* Raffinement de l'algorithme d'inférence de typeGravatar herbelin2007-09-17
* Réponse à une incompatibilité introduite dans 10114 (calcul du nombreGravatar herbelin2007-09-16
* Correction du bug #1679 (congruence) et ajout test-suiteGravatar corbinea2007-09-14
* Itération sur les sous-termes dans la vérification de la condition de gardeGravatar herbelin2007-09-06
* Extension et documentation de real_clean/evar_define dans evarutil.ml:Gravatar herbelin2007-08-25
* Correction du bug #1634 + ajout de bugs dans la test-suiteGravatar notin2007-08-22
* Correction du bug #1322Gravatar notin2007-08-16
* Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;Gravatar notin2007-08-16
* Ajout d'un exemple d'inversion des dépendances dans le prédicat commeGravatar herbelin2007-08-10
* TypoGravatar notin2007-08-10
* Modification de la test suite pour intégrer des tests spécifiques auxGravatar notin2007-08-10
* Add a test case for the new "dependent" induction tactics.Gravatar msozeau2007-08-08