| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins). |  Hugo Herbelin | 2017-01-22 |
| 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. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |