diff options
| author | Hugo Herbelin | 2015-08-21 19:45:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-08-21 20:20:01 +0200 |
| commit | 081a649157d2460c924404cd51b4ba50c23b1956 (patch) | |
| tree | 0a07d1cd8f6deff1061786654eb7c2225036fd82 | |
| 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.
| -rw-r--r-- | interp/constrintern.ml | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4318.v | 2 |
2 files changed, 4 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8c56d0ccfe..ecaf2b8c13 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1214,7 +1214,8 @@ let drop_notations_pattern looked_for = List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl, List.map2 (in_pat_sc env) argscs2 args) | NList (x,_,iter,terminator,lassoc) -> - let () = assert (List.is_empty args) in + if not (List.is_empty args) then user_err_loc + (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns."); (try (* All elements of the list are in scopes (scopt,subscopes) *) let (l,(scopt,subscopes)) = Id.Map.find x substlist in diff --git a/test-suite/bugs/closed/4318.v b/test-suite/bugs/closed/4318.v new file mode 100644 index 0000000000..e3140ed5ab --- /dev/null +++ b/test-suite/bugs/closed/4318.v @@ -0,0 +1,2 @@ +(* Check no anomaly is raised *) +Fail Definition foo p := match p with (x, y) z => tt end. |