| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fixing #4318 (anomaly when applying args to a recursive notation in patterns). |  Hugo Herbelin | 2015-08-21 |
| I don't know what was the intent of Pierre B here. In 8.4, it was not supported, raising with an error at parsing time. I changed the anomaly into an error at interpretation time, so it is still not supported but we could support it if some legitimate use of it eventually appears. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |