Fixing computation of non-recursively uniform arguments in the

presence of let-ins. This fixes #3491.

1 files changed, 4 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3491.v b/test-suite/bugs/closed/3491.v
new file mode 100644
index 000000000..fd394ddbc
--- /dev/null
+++ b/test-suite/bugs/closed/3491.v
@@ -0,0 +1,4 @@
+(* Was failing while building the _rect scheme, due to wrong computation of *)
+(* the number of non recursively uniform parameters in the presence of let-ins*)
+Inductive list (A : Type) (T := A) : Type :=
+    nil : list A | cons : T -> list T -> list A.