aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
Commit message (Expand)AuthorAge
* Add several reproduction files for bugs.Gravatar Xavier Clerc2014-09-25
* Update test-suite files.Gravatar Matthieu Sozeau2014-09-24
* Fix bug #3656.Gravatar Matthieu Sozeau2014-09-23
* Move the specific map_constr_with_binders_left_to_rightGravatar Matthieu Sozeau2014-09-19
* Fix constrMatching as well as change/e_contextually to allowGravatar Matthieu Sozeau2014-09-18
* Fix debug printing with primitive projections.Gravatar Matthieu Sozeau2014-09-18
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Fix bug #3633 properly, by delaying the interpetation of constrs inGravatar Matthieu Sozeau2014-09-17
* Revert "While resolving typeclass evars in clenv, touch only the ones that ap...Gravatar Matthieu Sozeau2014-09-17
* While resolving typeclass evars in clenv, touch only the ones that appear in theGravatar Matthieu Sozeau2014-09-17
* Update test-suite files after last commit. Add a file for rewrite_stratGravatar Matthieu Sozeau2014-09-17
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Fixing line break in test for #3559.Gravatar Hugo Herbelin2014-09-15
* Fixing injection bug #3616 on sigma-types.Gravatar Hugo Herbelin2014-09-13
* An old typo which was preventing example #3537 to work the same as itGravatar Hugo Herbelin2014-09-12
* Fix test-suite files, and move some opened to closed.Gravatar Matthieu Sozeau2014-09-11
* Fix bug #3594: eta for constructors and functions at the same time whichGravatar Matthieu Sozeau2014-09-11
* Fix bug #3596, wrong treatment of projections in compute_constelim_direct.Gravatar Matthieu Sozeau2014-09-11
* Fix bug #3505.Gravatar Matthieu Sozeau2014-09-11
* Test for "inversion as" naming bug.Gravatar Hugo Herbelin2014-09-07
* Regression test #3557Gravatar Hugo Herbelin2014-09-07
* Regression test for bug #2883.Gravatar Hugo Herbelin2014-09-07
* Fix bug #3584, elaborating pattern-matching on primitive records to theGravatar Matthieu Sozeau2014-09-06
* Status error for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
* Test for bug #3459.Gravatar Pierre-Marie Pédrot2014-09-04
* Fix bug #3561, correct folding of env in context[] matching.Gravatar Matthieu Sozeau2014-09-04
* Fix bug #3559, ensuring a canonical order of universe level quantifications whenGravatar Matthieu Sozeau2014-09-04
* Add test suite files for closed bugs.Gravatar Matthieu Sozeau2014-09-04
* Fix bug #3563, making syntactic matching of primitive projectionsGravatar Matthieu Sozeau2014-09-04
* Test-suite for bug #2818.Gravatar Pierre-Marie Pédrot2014-09-03
* Add test-suite file. Compute the name for the record binder in theGravatar Matthieu Sozeau2014-08-29
* Fix bugs #3484 and #3546.Gravatar Matthieu Sozeau2014-08-28
* There are some occurs-check cases that can be handled by imitation (using pru...Gravatar Matthieu Sozeau2014-08-28
* Adding test-suite for bug #3212.Gravatar Pierre-Marie Pédrot2014-08-28
* Add a regression test for 3427Gravatar Jason Gross2014-08-26
* Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleGravatar Matthieu Sozeau2014-08-25
* Fix computation of dangling constraints at the end of a proof (bug #3531).Gravatar Matthieu Sozeau2014-08-25
* Fix test-suite file.Gravatar Matthieu Sozeau2014-08-23
* Fix test-suite files.Gravatar Matthieu Sozeau2014-08-18
* Restrict eta-conversion to inductive records, fixing bug #3310.Gravatar Matthieu Sozeau2014-08-14
* Fix test-suite files according to new parsing rule for application of primitiveGravatar Matthieu Sozeau2014-08-13
* Bug #3469: fixing unterminated comment.Gravatar Hugo Herbelin2014-08-12
* In bug #2406, renouncing to test failure of parsing error.Gravatar Hugo Herbelin2014-08-12
* Fix unification which was failing when unifying a primitive projection againstGravatar Matthieu Sozeau2014-08-09
* Fix evarconv not applying eta when it used to. Fixes bug#3319.Gravatar Matthieu Sozeau2014-08-08
* Fixing #3483 (graceful failing with notations to non-constructors in "match").Gravatar Hugo Herbelin2014-08-03
* Finish fixes on notations and primitive projections, add test-suite files for...Gravatar Matthieu Sozeau2014-07-31
* Add test-suite file for bug #3439.Gravatar Matthieu Sozeau2014-07-30
* Add test-suite file for bug 3454.Gravatar Matthieu Sozeau2014-07-29
* Add test-suite file for bug #3453Gravatar Matthieu Sozeau2014-07-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 07:33:36 +0000