From 20bb249ed0e19cc0132519e3de06fafe2ba500c3 Mon Sep 17 00:00:00 2001
From: xclerc
Date: Fri, 20 Sep 2013 12:33:49 +0000
Subject: Get rid of "shouldfail" subdirectory by moving tests to parent
 directory.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16796 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/1703.v            |  8 ++++++++
 test-suite/bugs/closed/1898.v            |  6 ++++++
 test-suite/bugs/closed/1915.v            |  6 ++++++
 test-suite/bugs/closed/2006.v            | 23 +++++++++++++++++++++++
 test-suite/bugs/closed/2251.v            |  6 ++++++
 test-suite/bugs/closed/2406.v            |  3 +++
 test-suite/bugs/closed/2586.v            |  6 ++++++
 test-suite/bugs/closed/2846.v            |  3 +++
 test-suite/bugs/closed/shouldfail/1703.v |  8 --------
 test-suite/bugs/closed/shouldfail/1898.v |  6 ------
 test-suite/bugs/closed/shouldfail/1915.v |  6 ------
 test-suite/bugs/closed/shouldfail/2006.v | 23 -----------------------
 test-suite/bugs/closed/shouldfail/2251.v |  6 ------
 test-suite/bugs/closed/shouldfail/2406.v |  3 ---
 test-suite/bugs/closed/shouldfail/2586.v |  6 ------
 test-suite/bugs/closed/shouldfail/2846.v |  3 ---
 16 files changed, 61 insertions(+), 61 deletions(-)
 create mode 100644 test-suite/bugs/closed/1703.v
 create mode 100644 test-suite/bugs/closed/1898.v
 create mode 100644 test-suite/bugs/closed/1915.v
 create mode 100644 test-suite/bugs/closed/2006.v
 create mode 100644 test-suite/bugs/closed/2251.v
 create mode 100644 test-suite/bugs/closed/2406.v
 create mode 100644 test-suite/bugs/closed/2586.v
 create mode 100644 test-suite/bugs/closed/2846.v
 delete mode 100644 test-suite/bugs/closed/shouldfail/1703.v
 delete mode 100644 test-suite/bugs/closed/shouldfail/1898.v
 delete mode 100644 test-suite/bugs/closed/shouldfail/1915.v
 delete mode 100644 test-suite/bugs/closed/shouldfail/2006.v
 delete mode 100644 test-suite/bugs/closed/shouldfail/2251.v
 delete mode 100644 test-suite/bugs/closed/shouldfail/2406.v
 delete mode 100644 test-suite/bugs/closed/shouldfail/2586.v
 delete mode 100644 test-suite/bugs/closed/shouldfail/2846.v

diff --git a/test-suite/bugs/closed/1703.v b/test-suite/bugs/closed/1703.v
new file mode 100644
index 0000000000..114e3185b8
--- /dev/null
+++ b/test-suite/bugs/closed/1703.v
@@ -0,0 +1,8 @@
+(* Check correct binding of intros until used in Ltac *)
+
+Ltac intros_until n := intros until n.
+
+Goal forall i j m n : nat, i = 0 /\ j = 0 /\ m = 0 /\ n = 0.
+intro i.
+Fail intros until i.
+Abort.
diff --git a/test-suite/bugs/closed/1898.v b/test-suite/bugs/closed/1898.v
new file mode 100644
index 0000000000..70461286ce
--- /dev/null
+++ b/test-suite/bugs/closed/1898.v
@@ -0,0 +1,6 @@
+(* folding should not allow circular dependencies *)
+
+Lemma bug_fold_unfold : True.
+  set (h := 1).
+  Fail fold h in h.
+  Abort.
diff --git a/test-suite/bugs/closed/1915.v b/test-suite/bugs/closed/1915.v
new file mode 100644
index 0000000000..7e62437d7b
--- /dev/null
+++ b/test-suite/bugs/closed/1915.v
@@ -0,0 +1,6 @@
+
+Require Import Setoid.
+
+Fail Goal forall x, impl True (x = 0) -> x = 0 -> False.
+(*intros x H E.
+rewrite H in E.*)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/2006.v b/test-suite/bugs/closed/2006.v
new file mode 100644
index 0000000000..d353d0e2d6
--- /dev/null
+++ b/test-suite/bugs/closed/2006.v
@@ -0,0 +1,23 @@
+(* Take the type constraint on Record into account *)
+
+Definition Type1 := Type.
+Fail Record R : Type1 := { p:Type1 }. (* was accepted before trunk revision 11619 *)
+
+(*
+Remarks:
+
+- The behaviour was inconsistent with the one of Inductive, e.g.
+
+  Inductive R : Type1 := Build_R : Type1 -> R.
+
+  was correctly refused.
+
+- CoRN makes some use of the following configuration:
+
+  Definition CProp := Type.
+  Record R : CProp := { ... }.
+
+  CoRN may have to change the CProp definition into a notation if the
+  preservation of the former semantics of Record type constraints
+  turns to be required.
+*)
diff --git a/test-suite/bugs/closed/2251.v b/test-suite/bugs/closed/2251.v
new file mode 100644
index 0000000000..d0fa3f2b33
--- /dev/null
+++ b/test-suite/bugs/closed/2251.v
@@ -0,0 +1,6 @@
+(* Check that rewrite does not apply to single evars *)
+
+Lemma evar_rewrite : (forall a : nat, a = 0 -> True) -> True.
+intros; eapply H.  (* goal is  ?30 = nil  *)
+Fail rewrite plus_n_Sm.
+Abort.
diff --git a/test-suite/bugs/closed/2406.v b/test-suite/bugs/closed/2406.v
new file mode 100644
index 0000000000..d46fbabbbc
--- /dev/null
+++ b/test-suite/bugs/closed/2406.v
@@ -0,0 +1,3 @@
+(* Check correct handling of unsupported notations *)
+Notation "'’'" := (fun x => x) (at level 20).
+Fail Definition crash_the_rooster f := ’.
diff --git a/test-suite/bugs/closed/2586.v b/test-suite/bugs/closed/2586.v
new file mode 100644
index 0000000000..7e02e7f110
--- /dev/null
+++ b/test-suite/bugs/closed/2586.v
@@ -0,0 +1,6 @@
+Require Import Setoid SetoidClass Program.
+
+Goal forall `(Setoid nat) x y, x == y -> S x == S y.
+  intros.
+  Fail clsubst H0.
+  Abort.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/2846.v b/test-suite/bugs/closed/2846.v
new file mode 100644
index 0000000000..8d6d348a2e
--- /dev/null
+++ b/test-suite/bugs/closed/2846.v
@@ -0,0 +1,3 @@
+Variable R : Type.
+
+Fail Inductive I : R := c : R.
diff --git a/test-suite/bugs/closed/shouldfail/1703.v b/test-suite/bugs/closed/shouldfail/1703.v
deleted file mode 100644
index 114e3185b8..0000000000
--- a/test-suite/bugs/closed/shouldfail/1703.v
+++ /dev/null
@@ -1,8 +0,0 @@
-(* Check correct binding of intros until used in Ltac *)
-
-Ltac intros_until n := intros until n.
-
-Goal forall i j m n : nat, i = 0 /\ j = 0 /\ m = 0 /\ n = 0.
-intro i.
-Fail intros until i.
-Abort.
diff --git a/test-suite/bugs/closed/shouldfail/1898.v b/test-suite/bugs/closed/shouldfail/1898.v
deleted file mode 100644
index 70461286ce..0000000000
--- a/test-suite/bugs/closed/shouldfail/1898.v
+++ /dev/null
@@ -1,6 +0,0 @@
-(* folding should not allow circular dependencies *)
-
-Lemma bug_fold_unfold : True.
-  set (h := 1).
-  Fail fold h in h.
-  Abort.
diff --git a/test-suite/bugs/closed/shouldfail/1915.v b/test-suite/bugs/closed/shouldfail/1915.v
deleted file mode 100644
index 7e62437d7b..0000000000
--- a/test-suite/bugs/closed/shouldfail/1915.v
+++ /dev/null
@@ -1,6 +0,0 @@
-
-Require Import Setoid.
-
-Fail Goal forall x, impl True (x = 0) -> x = 0 -> False.
-(*intros x H E.
-rewrite H in E.*)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldfail/2006.v b/test-suite/bugs/closed/shouldfail/2006.v
deleted file mode 100644
index d353d0e2d6..0000000000
--- a/test-suite/bugs/closed/shouldfail/2006.v
+++ /dev/null
@@ -1,23 +0,0 @@
-(* Take the type constraint on Record into account *)
-
-Definition Type1 := Type.
-Fail Record R : Type1 := { p:Type1 }. (* was accepted before trunk revision 11619 *)
-
-(*
-Remarks:
-
-- The behaviour was inconsistent with the one of Inductive, e.g.
-
-  Inductive R : Type1 := Build_R : Type1 -> R.
-
-  was correctly refused.
-
-- CoRN makes some use of the following configuration:
-
-  Definition CProp := Type.
-  Record R : CProp := { ... }.
-
-  CoRN may have to change the CProp definition into a notation if the
-  preservation of the former semantics of Record type constraints
-  turns to be required.
-*)
diff --git a/test-suite/bugs/closed/shouldfail/2251.v b/test-suite/bugs/closed/shouldfail/2251.v
deleted file mode 100644
index d0fa3f2b33..0000000000
--- a/test-suite/bugs/closed/shouldfail/2251.v
+++ /dev/null
@@ -1,6 +0,0 @@
-(* Check that rewrite does not apply to single evars *)
-
-Lemma evar_rewrite : (forall a : nat, a = 0 -> True) -> True.
-intros; eapply H.  (* goal is  ?30 = nil  *)
-Fail rewrite plus_n_Sm.
-Abort.
diff --git a/test-suite/bugs/closed/shouldfail/2406.v b/test-suite/bugs/closed/shouldfail/2406.v
deleted file mode 100644
index d46fbabbbc..0000000000
--- a/test-suite/bugs/closed/shouldfail/2406.v
+++ /dev/null
@@ -1,3 +0,0 @@
-(* Check correct handling of unsupported notations *)
-Notation "'’'" := (fun x => x) (at level 20).
-Fail Definition crash_the_rooster f := ’.
diff --git a/test-suite/bugs/closed/shouldfail/2586.v b/test-suite/bugs/closed/shouldfail/2586.v
deleted file mode 100644
index 7e02e7f110..0000000000
--- a/test-suite/bugs/closed/shouldfail/2586.v
+++ /dev/null
@@ -1,6 +0,0 @@
-Require Import Setoid SetoidClass Program.
-
-Goal forall `(Setoid nat) x y, x == y -> S x == S y.
-  intros.
-  Fail clsubst H0.
-  Abort.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldfail/2846.v b/test-suite/bugs/closed/shouldfail/2846.v
deleted file mode 100644
index 8d6d348a2e..0000000000
--- a/test-suite/bugs/closed/shouldfail/2846.v
+++ /dev/null
@@ -1,3 +0,0 @@
-Variable R : Type.
-
-Fail Inductive I : R := c : R.
-- 
cgit v1.2.3