aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
AgeCommit message (Expand)Author
2014-06-08ind_tables: always declare side effects (Closes: HOTT#110)Enrico Tassi
2014-06-03A bug has been closed (HoTT/coq #105)Jason Gross
2014-05-16Fix unification of non-unfoldable primitive projections in evarconv.Matthieu Sozeau
2014-05-12Update various polyproj bugs w.r.t. latest trunkJason Gross
2014-05-10Add appropriate Fail(s) to opened bugsJason Gross
2014-05-10Move opened bugs to bugs/openedJason Gross
2014-05-09Refresh universes for Ltac's type_of, as the term can be used anywhere,Matthieu Sozeau
2014-05-06Add regression tests for univ. poly. and prim projJason Gross
2013-12-19Missing Fail in r16792Pierre Boutillier
2013-11-29Testsuite: flatten the 'bugs/opened' directory.xclerc
2013-09-20Use "Fail" rather than rely on exit code.xclerc
2013-01-18Unset Asymmetric Patternspboutill
2011-06-18r14204 and 14218 continued: completely removing test for bug #2490,herbelin
2011-06-18Partial backtrack on wrong r14204: bug #2490 still open.herbelin
2010-06-13Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"herbelin
2010-04-07Granting wish #2251 thanks to commit 12900 solved bug 1416.v (whichherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-03Temporarily disabling automatic test for bug 1338.vnotin
2008-05-07Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757herbelin
2008-04-17Bug squashing day !msozeau
2008-04-15Mises à jour bugs, CHANGES, code mortherbelin
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-02-01Ajout de 2 testsnotin
2008-01-24Fermeture du bug #1754notin
2008-01-23Ajout d'un test pour le mode déclaratif + test pour le bug #1776notin
2008-01-21Correction du bug #1754notin
2007-12-21Ajouts de quelques tests sur les bugsnotin
2007-12-11Test pour le bug #1754notin
2007-09-21Correction d'un bug dans check + ajout de testsnotin
2007-08-22Correction du bug #1634 + ajout de bugs dans la test-suitenotin
2007-08-16Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;notin
2007-08-10Modification de la test suite pour intégrer des tests spécifiques auxnotin