aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* Préférence donnée aux constantes qui ne sont pas des projectionsGravatar herbelin2008-06-29
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
* - Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Improve the dependent induction tactic to automatically find theGravatar msozeau2008-05-30
* Résolution bug #1850 sur notations avec niveaux inconnus deGravatar herbelin2008-05-26
* Retrait d'un test commité par erreur en 10947Gravatar herbelin2008-05-20
* Intégration de micromega ("omicron" pour fourier et sa variante sur Z,Gravatar herbelin2008-05-19
* Various fixes:Gravatar msozeau2008-05-15
* Résolution des problèmes ambigus d'inférence du type de retour desGravatar herbelin2008-05-14
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
* Contournement laborieux de la "feature" de camlp5 qui entrainait leGravatar herbelin2008-04-30
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* - 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