aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
AgeCommit message (Expand)Author
2015-10-21Removing test for bug #3956.Pierre-Marie Pédrot
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: fixed 3685 by side-effect :)Matthieu Sozeau
2015-10-02Univs: fix test-suite file for HoTT/coq bug #120Matthieu Sozeau
2015-07-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-28Tests for bugs #3509 and #3510.Pierre-Marie Pédrot
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-16Remove old test file for #3819 (now fixed).Maxime Dénès
2015-07-06Temporarily disable test file for #3922.Maxime Dénès
2015-06-29Fix test file for #4214 which was fixed by Hugo.Maxime Dénès
2015-06-29Better test case by PMP for #3948.Maxime Dénès
2015-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-18Removing test for opened bugs that were already present in the closed test-su...Pierre-Marie Pédrot
2015-05-18Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Pierre-Marie Pédrot
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-14#3953 now closed.Hugo Herbelin
2015-05-09Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).Hugo Herbelin
2015-05-09Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forHugo Herbelin
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-24Updating test-suite (see previous commit).Hugo Herbelin
2015-03-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-03-08Test for bug #2951.Pierre-Marie Pédrot
2015-03-04Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-03Fix test-suite file, this is open.Matthieu Sozeau
2015-03-03Add missing test-suite files and update gitignore.Matthieu Sozeau
2015-02-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-27Fix test for #3848, still open.Maxime Dénès
2015-02-27Moving test for #3467 to closed after PMP's fix.Maxime Dénès
2015-02-27Fix test-suite files for bugs #2456 and #3593, still open.Maxime Dénès
2015-02-27Moving tests for #2456 and #3593 to "opened" until they're fixed.Maxime Dénès
2015-02-27Moving test of #3848 to "opened".Maxime Dénès
2015-02-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-26Test for bug #3298.Pierre-Marie Pédrot
2015-02-26Moving test for bug #3681 as closed.Pierre-Marie Pédrot
2015-02-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-21Moving test for bug #3071.Pierre-Marie Pédrot
2015-02-21Removed tests for #3900 and #3944 as open bugs.Hugo Herbelin
2015-02-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-15Test for bug #3490.Pierre-Marie Pédrot
2015-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-11Adding test for bug #3786.Pierre-Marie Pédrot
2015-01-28Several reproduction cases for the test suite.Xavier Clerc
2015-01-28Several reproduction cases for the test suite.Xavier Clerc
2015-01-18Revert "Update test for #3363 now that Require is forbidden inside modules."Maxime Dénès
2015-01-17Revert "Update test for #3363 now that Require is forbidden inside modules."Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:15:13 +0000