aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-01-22 10:52:18 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-01-22 12:05:10 +0100
commite91ae93106b6bd6d92ef53ac18b04654485a8106 (patch)
tree30bfa5ada3f09a639f78130b0d5518ff4f266abe /test-suite/output
parent6ff62ec78d5517ec5905041fa2e4926e15ff89f0 (diff)
Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).
A cleaning done in ade2363e35 (Dec 2015) was hinting at bugs in typing a matching over a "catch-all" variable, when let-ins occur in the arity. However ade2363e35 failed to understand what was the correct fix, introducing instead the regressions mentioned in #5322 and #5324. This fixes all of #5322 and #5324, as well as the handling of let-ins in the arity. Thanks to Jason for helping in diagnosing the problem.
Diffstat (limited to 'test-suite/output')
0 files changed, 0 insertions, 0 deletions