From 00964706efe8f6b13e38b57ddb45fac516feb958 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 13 May 2017 23:31:08 +0200
Subject: Fixing bug #5222 (anomaly with "`pat" in the presence of scope
 delimiters).

We seized this opportunity to factorize the code for interning `pat
with more general pre-existing code.

More precisely: There was already a function to compute the free
variables of a pattern. Commit c6d9d4fb rewrote an approximation of it
and #5222 hits cases non-treated by this function. We remove the
partially-defined redundant code and use instead the existing code
since intern_cases_pattern, already called, was already doing this
computation. (In doing so, we discover a bug in merging names in the
presence of nested "as" clauses, which we fix in previous
commit. Additionally, intern_local_pattern was misleadingly overkill
to simply mean a folding on Id.Set.add and we avoid the detour.
---
 test-suite/bugs/closed/5522.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/5522.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3