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

8 files changed, 0 insertions, 61 deletions

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.