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 /interp | |
| 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 'interp')
| -rw-r--r-- | interp/constrintern.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8c56d0ccf..ecaf2b8c1 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 |