aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Expand)Author
2014-09-07Test for "inversion as" naming bug.Hugo Herbelin
2014-09-07Regression test #3557Hugo Herbelin
2014-09-07Regression test for bug #2883.Hugo Herbelin
2014-09-06Fix bug #3584, elaborating pattern-matching on primitive records to theMatthieu Sozeau
2014-09-04Status error for bug #3459.Pierre-Marie Pédrot
2014-09-04Test for bug #3459.Pierre-Marie Pédrot
2014-09-04Fix bug #3561, correct folding of env in context[] matching.Matthieu Sozeau
2014-09-04Fix bug #3559, ensuring a canonical order of universe level quantifications whenMatthieu Sozeau
2014-09-04Add test suite files for closed bugs.Matthieu Sozeau
2014-09-04Fix bug #3563, making syntactic matching of primitive projectionsMatthieu Sozeau
2014-09-03Test-suite for bug #2818.Pierre-Marie Pédrot
2014-08-29Add test-suite file. Compute the name for the record binder in theMatthieu Sozeau
2014-08-28Fix bugs #3484 and #3546.Matthieu Sozeau
2014-08-28There are some occurs-check cases that can be handled by imitation (using pru...Matthieu Sozeau
2014-08-28Adding test-suite for bug #3212.Pierre-Marie Pédrot
2014-08-26Add a regression test for 3427Jason Gross
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
2014-08-25Fix computation of dangling constraints at the end of a proof (bug #3531).Matthieu Sozeau
2014-08-23Fix test-suite file.Matthieu Sozeau
2014-08-18Fix test-suite files.Matthieu Sozeau
2014-08-14Restrict eta-conversion to inductive records, fixing bug #3310.Matthieu Sozeau
2014-08-13Fix test-suite files according to new parsing rule for application of primitiveMatthieu Sozeau
2014-08-12Bug #3469: fixing unterminated comment.Hugo Herbelin
2014-08-12In bug #2406, renouncing to test failure of parsing error.Hugo Herbelin
2014-08-09Fix unification which was failing when unifying a primitive projection againstMatthieu Sozeau
2014-08-08Fix evarconv not applying eta when it used to. Fixes bug#3319.Matthieu Sozeau
2014-08-03Fixing #3483 (graceful failing with notations to non-constructors in "match").Hugo Herbelin
2014-07-31Finish fixes on notations and primitive projections, add test-suite files for...Matthieu Sozeau
2014-07-30Add test-suite file for bug #3439.Matthieu Sozeau
2014-07-29Add test-suite file for bug 3454.Matthieu Sozeau
2014-07-29Add test-suite file for bug #3453Matthieu Sozeau
2014-07-21Adding a test-suite for bug #3422.Pierre-Marie Pédrot
2014-07-16Adding a test-suite for bug #3416.Pierre-Marie Pédrot
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-30Tests for bugs #2834 and #2994.Hugo Herbelin
2014-06-30Completing test for bug report #2830Hugo Herbelin
2014-06-28Quickly fixing bug #2996: typing functions now check when referring toHugo Herbelin
2014-06-26Fix bug # 3325 using canonical structure declarations where needed.Matthieu Sozeau
2014-06-26Fixed bug with new semantics of change.Matthieu Sozeau
2014-06-26Properly refresh the local hintdb database in case an external tactic changedMatthieu Sozeau
2014-06-26Bug #3329 is closed.Matthieu Sozeau
2014-06-263392 is now closed thanks to E. Tassi.Matthieu Sozeau
2014-06-26Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into Jaso...Matthieu Sozeau
2014-06-26Fix test-suite files.Matthieu Sozeau
2014-06-26Bug #3301 is closed, the projection cannot be defined anymore.Matthieu Sozeau
2014-06-26Fix test-suite file for bug # 3036, the unification has _never_ succeeded,Matthieu Sozeau
2014-06-26Change interface of refresh universes to get a pbty argument instead ofMatthieu Sozeau
2014-06-26Add an Unset Standard...Matthieu Sozeau
2014-06-23Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 22:04:16 +0000