diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-21 19:45:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-21 20:20:01 +0200 |
| commit | 081a649157d2460c924404cd51b4ba50c23b1956 (patch) | |
| tree | 0a07d1cd8f6deff1061786654eb7c2225036fd82 /.gitignore | |
| parent | 15e6e2d666252cad3c1e0de4622ef51c2830b6b8 (diff) | |
Fixing #4318 (anomaly when applying args to a recursive notation in patterns).
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.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions