aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Résolution bug #1850 sur notations avec niveaux inconnus deGravatar herbelin2008-05-26
* Strategy commands are now exportedGravatar barras2008-05-22
* Correction bugs ide undo et highlight (suite à typos)Gravatar herbelin2008-05-21
* Corrections d'erreurs rapportées par Frédéric Besson sur le précédentGravatar herbelin2008-05-20
* Léger backtrack sur commit coqide précédent (si la commande à annulerGravatar herbelin2008-05-20
* Fixed coqide bug #1856 that was introduced in revision 10915.Gravatar herbelin2008-05-20
* 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
* MAJ et bricoles diversesGravatar herbelin2008-05-12
* Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757Gravatar herbelin2008-05-07
* 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
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* 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
* - Fix bug in eterm which was not taking filtered contexts in evars intoGravatar msozeau2008-04-25
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* fixed universes bug related to module inclusionGravatar barras2008-04-22
* test module include w.r.t. universe constraintsGravatar barras2008-04-21
* - Correct unification for the rewrite variant of setoid_rewrite,Gravatar msozeau2008-04-21
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Bug squashing day !Gravatar msozeau2008-04-17
* Mises à jour bugs, CHANGES, code mortGravatar herbelin2008-04-15
* - 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
* Correction du bug 1816 (ajout d'un lemme dans Znat) et suppressionGravatar notin2008-03-28
* Diverses petites modifs dans la test-suite:Gravatar notin2008-03-26
* Correction de bugs relatifs a la compostion des substitutionsGravatar soubiran2008-03-25
* Add the possibility of specifying constants to unfold for typeclassGravatar msozeau2008-03-17
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
* 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
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06