Merge branch 'v8.5' into trunk

5 files changed, 53 insertions, 2 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 4a3a287c08..cffbe48196 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -273,6 +273,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
+	    | grep -v "^<W>" \
 	    > $$tmpoutput; \
 	  diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
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/bugs/closed/4165.v b/test-suite/bugs/closed/4165.v
new file mode 100644
index 0000000000..8e0a62d35c
--- /dev/null
+++ b/test-suite/bugs/closed/4165.v
@@ -0,0 +1,7 @@
+Lemma foo : True.
+Proof.
+pose (fun x : nat => (let H:=true in x)) as s.
+match eval cbv delta [s] in s with
+| context C[true] =>
+  let C':=context C[false] in pose C' as s'
+end.
diff --git a/test-suite/bugs/opened/3491.v b/test-suite/bugs/opened/3491.v
deleted file mode 100644
index 9837b0ecb2..0000000000
--- a/test-suite/bugs/opened/3491.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Fail 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 3d4257543a..9661b3bfac 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -121,3 +121,44 @@ Inductive foo1 : forall p, Prop := cc1 : foo1 0.
 (* Check cross inference of evars from constructors *)
 
 Inductive foo2 : forall p, Prop := cc2 : forall q, foo2 q | cc3 : foo2 0.
+
+(* An example with reduction removing an occurrence of the inductive type in one of its argument *)
+
+Inductive IND1 (A:Type) := CONS1 : IND1 ((fun x => A) IND1).
+
+(* 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.
+
+(* An example of nested positivity which was rejected by the kernel
+   before 24 March 2015 (even with Unset Elimination Schemes to avoid
+   the _rect bug) due to the wrong computation of non-recursively
+   uniform parameters in list' *)
+
+Inductive list' (A:Type) (B:=A) :=
+| nil' : list' A
+| cons' : A -> list' B -> list' A.
+
+Inductive tree := node : list' tree -> tree.
+
+(* This type was raising an anomaly when building the _rect scheme,
+   because of a bug in Inductiveops.get_arity in the presence of
+   let-ins and recursively non-uniform parameters. *)
+
+Inductive L (A:Type) (T:=A) : Type := C : L nat -> L 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 when conversion is needed, leading the example to
+   hit the Inductiveops.get_arity bug mentioned above (see #3491) *)
+
+Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A.