Fixing #5755 (discharging of inductive types not correct with let-ins).

The number of effective parameters was used where the number of
declarations in the signature of parameters should have been used.

1 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5755.v b/test-suite/bugs/closed/5755.v
new file mode 100644
index 0000000000..e07fdcf831
--- /dev/null
+++ b/test-suite/bugs/closed/5755.v
@@ -0,0 +1,16 @@
+(* Sections taking care of let-ins for inductive types *)
+
+Section Foo.
+
+Inductive foo (A : Type) (x : A) (y := x) (y : A) := Foo.
+
+End Foo.
+
+Section Foo2.
+
+Variable B : Type.
+Variable b : B.
+Let c := b.
+Inductive foo2 (A : Type) (x : A) (y := x) (y : A) := Foo2 : c=c -> foo2 A x y.
+
+End Foo2.