aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2008-06-09- Documentation de admit et Print Assumptions.herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-06-05Renommage id dans le test Nametab (suite ajout d'une constante de ceherbelin
2008-06-03Temporarily disabling automatic test for bug 1338.vnotin
2008-05-30Improve the dependent induction tactic to automatically find themsozeau
2008-05-29fixed bug #1780: a lift was missing (match predicate)barras
2008-05-28- Correction bug highlighting "Module" dans Coqideherbelin
2008-05-26Résolution bug #1850 sur notations avec niveaux inconnus deherbelin
2008-05-22Strategy commands are now exportedbarras
2008-05-21Correction bugs ide undo et highlight (suite à typos)herbelin
2008-05-20Corrections d'erreurs rapportées par Frédéric Besson sur le précédentherbelin
2008-05-20Léger backtrack sur commit coqide précédent (si la commande à annulerherbelin
2008-05-20Fixed coqide bug #1856 that was introduced in revision 10915.herbelin
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-12MAJ et bricoles diversesherbelin
2008-05-07Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757herbelin
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-28Backtrack on using metas eagerly in auto, only done in "new auto" formsozeau
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-25- Fix bug in eterm which was not taking filtered contexts in evars intomsozeau
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-22fixed universes bug related to module inclusionbarras
2008-04-21test module include w.r.t. universe constraintsbarras
2008-04-21- Correct unification for the rewrite variant of setoid_rewrite,msozeau
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
2008-04-17Bug squashing day !msozeau
2008-04-15Mises à jour bugs, CHANGES, code mortherbelin
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-28Correction du bug 1816 (ajout d'un lemme dans Znat) et suppressionnotin
2008-03-26Diverses petites modifs dans la test-suite:notin
2008-03-25Correction de bugs relatifs a la compostion des substitutionssoubiran
2008-03-17Add the possibility of specifying constants to unfold for typeclassmsozeau
2008-03-16Using the "relation" constant made some unifications fail in the newmsozeau
2008-03-16Misc: Add test for bug 1704, now closed. Add usual syntax for lists inmsozeau