Fixing computation of non-recursively uniform arguments in the

presence of let-ins. This fixes #3491.

3 files changed, 20 insertions, 1 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 49bf3281fe..6b909824ba 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -485,6 +485,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 	          check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
 	| Rel k ->
             (try let (ra,rarg) = List.nth ra_env (k-1) in
+            let largs = List.map (whd_betadeltaiota env) largs in
 	    let nmr1 =
 	      (match ra with
                   Mrec _ -> compute_rec_par ienv hyps nmr largs
diff --git a/test-suite/bugs/closed/3491.v b/test-suite/bugs/closed/3491.v
new file mode 100644
index 0000000000..fd394ddbc3
--- /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.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 04d92daad9..de18ed96ef 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -126,7 +126,21 @@ Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0.
 
 Inductive IND1 (A:Type) := CONS1 : IND1 ((fun x => A) IND1).
 
-(* This type was considered as ill-formed before March 2015, while it
+(* These types were considered as ill-formed before March 2015, while they
    could be accepted considering that the type IND1 above was accepted *)
 
 Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2).
+
+Inductive IND3 (A:Type) (T:=fun _ : Type->Type => A) := CONS3 : IND3 (T IND3) -> IND3 A.
+
+Inductive IND4 (A:Type) := CONS4 : IND4 ((fun x => A) IND4) -> IND4 A.
+
+(* This type was ok before March 2015 *)
+
+Inductive IND5 (A : Type) (T := A) : Type := CONS5 : IND5 ((fun _ => A) 0) -> IND5 A.
+
+(* This type was raising an anomaly when building the _rect scheme,
+   because of a wrong computation of the number of non-recursively
+   uniform parameters in the presence of let-ins (see #3491) *)
+
+Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A.