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

2 files changed, 12 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.
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 49c465b6c6..52fe98ac07 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1868,3 +1868,8 @@ Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
 Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end.
 
 Check match niln in listn O return O=O with niln => eq_refl end.
+
+(* A test about nested "as" clauses *)
+(* (was failing up to May 2017) *)
+
+Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end.