1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1477.v b/test-suite/bugs/closed/shouldsucceed/1477.v
new file mode 100644
index 00000000..dfc8c328
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1477.v
@@ -0,0 +1,18 @@
+Inductive I : Set :=
+  | A : nat -> nat -> I
+  | B : nat -> nat -> I.
+
+Definition foo1 (x:I) : nat :=
+  match x with
+    | A a b | B a b => S b
+  end.
+
+Definition foo2 (x:I) : nat :=
+  match x with
+    | A _ b | B b _ => S b
+  end.
+
+Definition foo (x:I) : nat :=
+  match x with
+    | A a b | B b a => S b
+  end.