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

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

2 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3210.v b/test-suite/bugs/closed/3210.v
new file mode 100644
index 0000000000..e66bf922d7
--- /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.
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 4eb2dbe9f5..ce9050d421 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -5,3 +5,15 @@ Lemma a : forall x:I eq_refl, match x in I a b c return b = b with C => eq_refl
 intro.
 match goal with |- ?c => let x := eval cbv in c in change x end.
 Abort.
+
+Check forall x:I eq_refl, match x in I x return x = x with C => eq_refl end = eq_refl.
+
+(* This is bug #3210 *)
+
+Inductive I' : let X := Set in X :=
+| C' : I'.
+
+Definition foo (x : I') : bool :=
+  match x with
+  C' => true
+  end.