Merge "inductive?.v" tests into a single "inductive.v" test.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16798 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 12 insertions, 13 deletions

diff --git a/test-suite/failure/inductive4.v b/test-suite/failure/inductive.v
index 4563490dc..143e8bb36 100644
--- a/test-suite/failure/inductive4.v
+++ b/test-suite/failure/inductive.v
@@ -1,3 +1,15 @@
+(* A check that sort-polymorphic product is not set too low *)
+
+Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
+Fail Check (fun (A:Type) (B:Prop) => (prod A B : Prop)).
+Fail Check (fun (A:Prop) (B:Type) => (prod A B : Prop)).
+
+(* Check that the nested inductive types positivity check avoids recursively
+   non uniform parameters (at least if these parameters break positivity) *)
+
+Inductive t (A:Type) : Type := c : t (A -> A) -> t A.
+Fail Inductive u : Type := d : u | e : t u -> u.
+
 (* This used to succeed in versions 8.1 to 8.3 *)
 
 Require Import Logic.
diff --git a/test-suite/failure/inductive1.v b/test-suite/failure/inductive1.v
deleted file mode 100644
index 7f42e7e16..000000000
--- a/test-suite/failure/inductive1.v
+++ /dev/null
@@ -1,4 +0,0 @@
-(* A check that sort-polymorphic product is not set too low *)
-
-Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
-Fail Check (fun (A:Type) (B:Prop) => (prod A B : Prop)).
diff --git a/test-suite/failure/inductive2.v b/test-suite/failure/inductive2.v
deleted file mode 100644
index 827c6f9fa..000000000
--- a/test-suite/failure/inductive2.v
+++ /dev/null
@@ -1,4 +0,0 @@
-(* A check that sort-polymorphic product is not set too low *)
-
-Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
-Fail Check (fun (A:Prop) (B:Type) => (prod A B : Prop)).
diff --git a/test-suite/failure/inductive3.v b/test-suite/failure/inductive3.v
deleted file mode 100644
index aacc9df71..000000000
--- a/test-suite/failure/inductive3.v
+++ /dev/null
@@ -1,5 +0,0 @@
-(* Check that the nested inductive types positivity check avoids recursively
-   non uniform parameters (at least if these parameters break positivity) *)
-
-Inductive t (A:Type) : Type := c : t (A -> A) -> t A.
-Fail Inductive u : Type := d : u | e : t u -> u.