diff options
| -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. |