aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
* Fix setoid tests, use red for a Setoid_Theory lemma, and ParametricGravatar msozeau2008-04-14
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Correction problème de compil (blast.ml)Gravatar herbelin2008-04-04
* Chgts mineurs:Gravatar herbelin2008-04-03
* Minor fixes. Use expanded type in class_tactics for Morphism search, toGravatar msozeau2008-04-02
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Fix test-suite files, change conflicting notation "->rel" and the othersGravatar msozeau2008-03-29
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Diverses petites modifs dans la test-suite:Gravatar notin2008-03-26
* Misc: Add test for bug 1704, now closed. Add usual syntax for lists inGravatar msozeau2008-03-16
* Forgot the test file.Gravatar msozeau2008-03-15
* Backtrack sur le test censé discriminer entre une erreur d'evar nonGravatar herbelin2008-03-15
* 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
* 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
* Correction d'un bug de clearGravatar notin2008-02-11
* Correction d'un bug à l'interprétation de "change" (on exigeait queGravatar herbelin2008-02-06
* 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
* Ajout d'un test pour le mode déclaratif + test pour le bug #1776Gravatar notin2008-01-23
* Better resolution of implicit parameters in typeclass binders, add extensiona...Gravatar msozeau2008-01-02
* Complément aux commits 10124 et 10125 sur l'inférence de type (correction Gravatar herbelin2007-09-26
* 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
* Extension et documentation de real_clean/evar_define dans evarutil.ml:Gravatar herbelin2007-08-25
* Ajout d'un exemple d'inversion des dépendances dans le prédicat commeGravatar herbelin2007-08-10
* Add a test case for the new "dependent" induction tactics.Gravatar msozeau2007-08-08
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
* Improvements / Bug fixes for ROmega Gravatar letouzey2007-07-09
* Contrôle de la compatibilité de apply via une information dans lesGravatar herbelin2007-05-28
* Unification suite: petits affinements pour préserver la compatibilitéGravatar herbelin2007-05-24
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* Wish #1582 (3eme)Gravatar herbelin2007-05-18
* Correction bug calcul des implicites en présence d'evars dans les typesGravatar herbelin2007-05-16
* Modification syntaxe de TestGravatar herbelin2007-04-30
* Correction bug #1507 (report révision 9807 de v8.1 vers trunk)Gravatar herbelin2007-04-29
* Correction bug #1477 sur ordre des variables partagées par les or-patterns.Gravatar herbelin2007-04-13
* Test non régression bug #1491Gravatar herbelin2007-04-13
* Test de non-régression pour commit 9673Gravatar herbelin2007-03-15