aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
AgeCommit message (Expand)Author
2014-06-17Explicit universes allow to write liftings explicitely. Implicit lifting woul...Matthieu Sozeau
2014-06-17Not considering test-suite file #89 as a bug anymore.Matthieu Sozeau
2014-06-17Continue fix on argument scopes of primitive projections.Matthieu Sozeau
2014-06-17Fix HoTT bug #84, binding scopes to projections.Matthieu Sozeau
2014-06-17HoTT coq bug #82 already fixed.Matthieu Sozeau
2014-06-17Adapt coercion code to work with projections as target classes.Matthieu Sozeau
2014-06-17- Fix the de Bruijn problem in check_projection for good :)Matthieu Sozeau
2014-06-17Fix a de Bruijn bug in checking code of projections.Matthieu Sozeau
2014-06-17Existing Class now works with universe polymorphism. Fixes HoTT bug #063Matthieu Sozeau
2014-06-16Unification in HoTT_coq_061.v was looping with previous commit (whileHugo Herbelin
2014-06-16- Add "Show Universes" to print information about universes during a proof.Matthieu Sozeau
2014-06-16HoTT bug #29 is fixed, using the correct notion of polymorphic product types.Matthieu Sozeau
2014-06-15Change Ltac constr matching semantics to consider universes when merging twoMatthieu Sozeau
2014-06-15The semantics of Variable x y : T is to have the exact same type T for x and y,Matthieu Sozeau
2014-06-15Remove HoTT bug #33, as the stdlib won't become polymorphic in the next version.Matthieu Sozeau
2014-06-15- Fix xml plugin treatment of inductives.Matthieu Sozeau
2014-06-13Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead of...Matthieu Sozeau
2014-06-13HoTT/coq bug #7 is closed, and the definitions can be made to go through usin...Matthieu Sozeau
2014-06-11Fix bug #3291, stack overflow in rewrite.Matthieu Sozeau
2014-06-11Fix bug #3289Matthieu Sozeau
2014-06-11Move bug # 3368 to closed bugsMatthieu Sozeau
2014-06-10Add many more cases to the test-suiteJason Gross
2014-06-10Move closed bug 3314Jason Gross
2014-06-10Add a test-case for bug #3314 proving FalseJason Gross
2014-06-08Mark some progress in the HoTT/coq test-suiteJason Gross
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 14:30:45 +0000