Fixing first part of bug #3210 (inference of pattern-matching return

clause in the presence of let-ins in the arity of inductive type).

1 files changed, 9 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3210.v b/test-suite/bugs/closed/3210.v
new file mode 100644
index 000000000..e66bf922d
--- /dev/null
+++ b/test-suite/bugs/closed/3210.v
@@ -0,0 +1,9 @@
+(* Test support of let-in in arity of inductive types *)
+
+Inductive Foo : let X := Set in X :=
+| I : Foo.
+
+Definition foo (x : Foo) : bool :=
+  match x with
+  I => true
+  end.