Merge PR#635: Fixing #5522 (anomaly with free vars of pat)

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 0000000000..0fae9ede42
--- /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.