aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
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
* 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
* Correction typo liée au commit 8779 (levait une anomalie)Gravatar herbelin2007-02-21
* Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGESGravatar herbelin2007-02-21
* Réparation absence d'interprétation des liaisons vers listesGravatar herbelin2007-02-15
* Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deGravatar herbelin2007-02-13
* Report de la révision 9577 dans le trunkGravatar notin2007-02-01
* Redondance erronée dans les testsGravatar herbelin2007-01-25
* Correction d'un bug d'unification-pattern dans l'algo d'unificationGravatar herbelin2007-01-22
* Correction pour le rapport de bug #1325 par rétablissement duGravatar herbelin2007-01-22
* Suite au mail de Lionel a propos du Makefile: Gravatar letouzey2007-01-12
* Alignement de la politique de renommage de rename_bound_var (utilisé pourGravatar herbelin2006-12-13
* Dépliage du terme d'induction avant suppression quand celui-ci est unGravatar herbelin2006-12-13
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
* Raffinement de l'unification de "apply": mémorisation de certainsGravatar herbelin2006-11-19
* Correction typoGravatar herbelin2006-11-13