aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
AgeCommit message (Expand)Author
2016-01-12Fixing #4256 and #4484 (changes in evar-evar resolution made that newHugo Herbelin
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-11Now closed.Matthieu Sozeau
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
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-28Tests for bugs #3509 and #3510.Pierre-Marie Pédrot
2015-07-16Remove old test file for #3819 (now fixed).Maxime Dénès
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-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-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-03-24Updating test-suite (see previous commit).Hugo Herbelin
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-03Fix test-suite file, this is open.Matthieu Sozeau
2015-03-03Add missing test-suite files and update gitignore.Matthieu Sozeau
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-26Test for bug #3298.Pierre-Marie Pédrot
2015-02-26Moving test for bug #3681 as closed.Pierre-Marie Pédrot
2015-02-21Moving test for bug #3071.Pierre-Marie Pédrot
2015-02-15Test for bug #3490.Pierre-Marie Pédrot
2015-02-11Adding test for bug #3786.Pierre-Marie Pédrot
2015-01-17Revert "Update test for #3363 now that Require is forbidden inside modules."Maxime Dénès
2015-01-12Update test for #3363 now that Require is forbidden inside modules.Maxime Dénès
2014-12-19Fixing wrong notation level in #3295.Hugo Herbelin
2014-12-16#3828 is solved.Hugo Herbelin
2014-12-16Moving #2447 (congruence) to fixed.Hugo Herbelin
2014-12-11New reproduction cases for the test suite.Xavier Clerc
2014-12-05Commits on evar-evar unification fixed HoTT_coq_106 and improved theHugo Herbelin
2014-11-30Adding test for bug #3417.Pierre-Marie Pédrot
2014-11-30Test for bug #3487.Pierre-Marie Pédrot
2014-11-30Test of bug #3682.Pierre-Marie Pédrot
2014-11-25Bug #3804 is actually closed (thanks to Jason Gross for the notification).Xavier Clerc
2014-11-25Tweak some test cases.Xavier Clerc
2014-11-24Adding test for bug #3248.Pierre-Marie Pédrot
2014-11-21Cleaning up closed bugs in test-suite.Pierre-Marie Pédrot
2014-11-14Add missing "Fail" to test case for bug #2814.Xavier Clerc
2014-11-14Reproduction cases for the test suite.Xavier Clerc
2014-11-08Test #3655 was failing due to an anomaly. Now it rather has to failHugo Herbelin
2014-11-08Test fixed by PMP's commits from Oct 21.Hugo Herbelin
2014-11-04test suite: some reproduction cases for recently-reported bugs.Xavier Clerc
2014-11-03New bugs revealed fixed: #3408 by (probably) Maxime's commitsHugo Herbelin
2014-10-21More precise test for #3459.Hugo Herbelin
2014-10-16Bug fixed by Hugo.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 01:38:01 +0000