aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
AgeCommit message (Expand)Author
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
2014-10-15Adding a timeout to bug #2447.Pierre-Marie Pédrot
2014-10-15Fix for bug #3618.Matthieu Sozeau
2014-10-15Bug 3692 is fixed.Matthieu Sozeau
2014-10-15Bug 3628 is fixed.Matthieu Sozeau
2014-10-03Add a bunch of reproduction files for bugs.Xavier Clerc
2014-09-30Add a bunch of reproduction files for bugs.Xavier Clerc
2014-09-29In evarconv and unification, expand folded primitive projections toMatthieu Sozeau
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-26Add a bunch of reproduction files for bugs.Xavier Clerc
2014-09-26Add missing "Fail" to bug cases.Xavier Clerc
2014-09-26Bug #3566 is fixed.Xavier Clerc
2014-09-25Add several reproduction files for bugs.Xavier Clerc
2014-09-24Update test-suite files.Matthieu Sozeau
2014-09-17Update test-suite files after last commit. Add a file for rewrite_stratMatthieu Sozeau
2014-09-17Revert specific syntax for primitive projections, avoiding uglyMatthieu Sozeau
2014-09-11Fix test-suite files, and move some opened to closed.Matthieu Sozeau
2014-09-04Status error for bug #3459.Pierre-Marie Pédrot
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
2014-08-18Fix test-suite file.Matthieu Sozeau
2014-08-14Restrict eta-conversion to inductive records, fixing bug #3310.Matthieu Sozeau
2014-08-08Fix evarconv not applying eta when it used to. Fixes bug#3319.Matthieu Sozeau
2014-07-03Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl...Matthieu Sozeau
2014-07-02Indeed simpl never is really honored now.Matthieu Sozeau
2014-06-26Invalid bug report.Matthieu Sozeau
2014-06-26Fix bug # 3325 using canonical structure declarations where needed.Matthieu Sozeau
2014-06-26Add an option to disable typeclass resolution during conversion, whichMatthieu Sozeau
2014-06-26Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into JasonG...Matthieu Sozeau
2014-06-26Fixed bug with new semantics of change.Matthieu Sozeau