From 4ac92a2aebe31ff4d5d2fce48701e5994391d7b9 Mon Sep 17 00:00:00 2001
From: xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 20 Sep 2013 12:55:35 +0000
Subject: 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
---
 test-suite/failure/inductive.v  | 27 +++++++++++++++++++++++++++
 test-suite/failure/inductive1.v |  4 ----
 test-suite/failure/inductive2.v |  4 ----
 test-suite/failure/inductive3.v |  5 -----
 test-suite/failure/inductive4.v | 15 ---------------
 5 files changed, 27 insertions(+), 28 deletions(-)
 create mode 100644 test-suite/failure/inductive.v
 delete mode 100644 test-suite/failure/inductive1.v
 delete mode 100644 test-suite/failure/inductive2.v
 delete mode 100644 test-suite/failure/inductive3.v
 delete mode 100644 test-suite/failure/inductive4.v

(limited to 'test-suite/failure')

diff --git a/test-suite/failure/inductive.v b/test-suite/failure/inductive.v
new file mode 100644
index 000000000..143e8bb36
--- /dev/null
+++ b/test-suite/failure/inductive.v
@@ -0,0 +1,27 @@
+(* 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.
+Require Hurkens.
+Definition Ti := Type.
+Inductive prod (X Y:Ti) := pair : X -> Y -> prod X Y.
+Fail Definition B : Prop := let F := prod True in F Prop. (* Aie! *)
+(*Definition p2b (P:Prop) : B := pair True Prop I P.
+Definition b2p (b:B) : Prop := match b with pair _ P => P end.
+Lemma L1 : forall A : Prop, b2p (p2b A) -> A.
+Proof (fun A x => x).
+Lemma L2 : forall A : Prop, A -> b2p (p2b A).
+Proof (fun A x => x).
+Check Hurkens.paradox B p2b b2p L1 L2.*)
+
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.
diff --git a/test-suite/failure/inductive4.v b/test-suite/failure/inductive4.v
deleted file mode 100644
index 4563490dc..000000000
--- a/test-suite/failure/inductive4.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(* This used to succeed in versions 8.1 to 8.3 *)
-
-Require Import Logic.
-Require Hurkens.
-Definition Ti := Type.
-Inductive prod (X Y:Ti) := pair : X -> Y -> prod X Y.
-Fail Definition B : Prop := let F := prod True in F Prop. (* Aie! *)
-(*Definition p2b (P:Prop) : B := pair True Prop I P.
-Definition b2p (b:B) : Prop := match b with pair _ P => P end.
-Lemma L1 : forall A : Prop, b2p (p2b A) -> A.
-Proof (fun A x => x).
-Lemma L2 : forall A : Prop, A -> b2p (p2b A).
-Proof (fun A x => x).
-Check Hurkens.paradox B p2b b2p L1 L2.*)
-
-- 
cgit v1.2.3