1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5322.v b/test-suite/bugs/closed/5322.v
new file mode 100644
index 00000000..01aec8f2
--- /dev/null
+++ b/test-suite/bugs/closed/5322.v
@@ -0,0 +1,14 @@
+(* Regression in computing types of branches in "match" *)
+Inductive flat_type := Unit | Prod (A B : flat_type).
+Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type
+-> Type :=
+| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR.
+Inductive op : flat_type -> flat_type -> Type := a : op Unit Unit.
+Arguments Op {_ _ _ _} _ _.
+Definition bound_op {var}
+           {src2 dst2}
+           (opc2 : op src2 dst2)
+  : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2.
+  refine match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with
+         | _ => _
+         end.