From 0b8d185baab95d92a7779482c7861c7be0a8e979 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 9 Feb 2017 18:26:33 +0100
Subject: Fixing bug #5346 (an unimplemented application of 'pat).

---
 test-suite/bugs/closed/5346.v | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 test-suite/bugs/closed/5346.v

diff --git a/test-suite/bugs/closed/5346.v b/test-suite/bugs/closed/5346.v
new file mode 100644
index 0000000000..0118c18704
--- /dev/null
+++ b/test-suite/bugs/closed/5346.v
@@ -0,0 +1,29 @@
+Inductive comp : Type -> Type :=
+| Ret {T} : forall (v:T), comp T
+| Bind {T T'} : forall (p: comp T') (p': T' -> comp T), comp T.
+
+Notation "'do' x .. y <- p1 ; p2" :=
+  (Bind p1 (fun x => .. (fun y => p2) ..))
+    (at level 60, right associativity,
+     x binder, y binder).
+
+Definition Fst1 A B (p: comp (A*B)) : comp A :=
+  do '(a, b) <- p;
+    Ret a.
+
+Definition Fst2 A B (p: comp (A*B)) : comp A :=
+  match tt with
+  | _ => Bind p (fun '(a, b) => Ret a)
+  end.
+
+Definition Fst3 A B (p: comp (A*B)) : comp A :=
+  match tt with
+  | _ => do a <- p;
+          Ret (fst a)
+  end.
+
+Definition Fst A B (p: comp (A * B)) : comp A :=
+  match tt with
+  | _ => do '(a, b) <- p;
+          Ret a
+  end.
-- 
cgit v1.2.3