From e2de94b90e8802fa5c5dc33c7daf6b8ce5646bfa Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 14 May 2017 00:10:57 +0200
Subject: Fixing a bug with nested "as" clauses in "match".

---
 test-suite/success/Cases.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite')

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