aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2008-05-20Retrait d'un test commité par erreur en 10947herbelin
2008-05-19Intégration de micromega ("omicron" pour fourier et sa variante sur Z,herbelin
2008-05-15Various fixes:msozeau
2008-05-14Résolution des problèmes ambigus d'inférence du type de retour desherbelin
2008-05-05Mise en place d'un algorithme d'inversion des contraintes de type lorsherbelin
2008-05-01Clarification de l'ordre d'interprétation des variables dans ltac. Enherbelin
2008-04-30Contournement laborieux de la "feature" de camlp5 qui entrainait leherbelin
2008-04-28Petites corrections vis à vis des commits 10860, 10859, 10850herbelin
2008-04-27Quelques bricoles autour de l'unification:herbelin
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-15- Un peu de doc, préparation du CHANGES pour la release.herbelin
2008-04-14Fix setoid tests, use red for a Setoid_Theory lemma, and Parametricmsozeau
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-04Correction problème de compil (blast.ml)herbelin
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