diff options
Diffstat (limited to 'test-suite/bugs/closed/5522.v')
| -rw-r--r-- | test-suite/bugs/closed/5522.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5522.v b/test-suite/bugs/closed/5522.v new file mode 100644 index 00000000..0fae9ede --- /dev/null +++ b/test-suite/bugs/closed/5522.v @@ -0,0 +1,7 @@ +(* Checking support for scope delimiters and as clauses in 'pat + applied to notations with binders *) + +Notation "'multifun' x .. y 'in' f" := (fun x => .. (fun y => f) .. ) + (at level 200, x binder, y binder, f at level 200). + +Check multifun '((x, y)%core as z) in (x+y,0)=z. |