Use "Fail" rather than rely on exit code.

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

7 files changed, 13 insertions, 9 deletions

diff --git a/test-suite/bugs/closed/shouldfail/1703.v b/test-suite/bugs/closed/shouldfail/1703.v
index 6b5198cc0..114e3185b 100644
--- a/test-suite/bugs/closed/shouldfail/1703.v
+++ b/test-suite/bugs/closed/shouldfail/1703.v
@@ -4,4 +4,5 @@ Ltac intros_until n := intros until n.
 
 Goal forall i j m n : nat, i = 0 /\ j = 0 /\ m = 0 /\ n = 0.
 intro i.
-intros until i.
+Fail intros until i.
+Abort.
diff --git a/test-suite/bugs/closed/shouldfail/1898.v b/test-suite/bugs/closed/shouldfail/1898.v
index 92490eb94..70461286c 100644
--- a/test-suite/bugs/closed/shouldfail/1898.v
+++ b/test-suite/bugs/closed/shouldfail/1898.v
@@ -2,4 +2,5 @@
 
 Lemma bug_fold_unfold : True.
   set (h := 1).
-  fold h in h.
+  Fail fold h in h.
+  Abort.
diff --git a/test-suite/bugs/closed/shouldfail/1915.v b/test-suite/bugs/closed/shouldfail/1915.v
index a96a482c6..7e62437d7 100644
--- a/test-suite/bugs/closed/shouldfail/1915.v
+++ b/test-suite/bugs/closed/shouldfail/1915.v
@@ -1,6 +1,6 @@
 
 Require Import Setoid.
 
-Goal forall x, impl True (x = 0) -> x = 0 -> False.
-intros x H E.
-rewrite H in E.
\ No newline at end of file
+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
index 91a16f955..d353d0e2d 100644
--- a/test-suite/bugs/closed/shouldfail/2006.v
+++ b/test-suite/bugs/closed/shouldfail/2006.v
@@ -1,7 +1,7 @@
 (* Take the type constraint on Record into account *)
 
 Definition Type1 := Type.
-Record R : Type1 := { p:Type1 }. (* was accepted before trunk revision 11619 *)
+Fail Record R : Type1 := { p:Type1 }. (* was accepted before trunk revision 11619 *)
 
 (*
 Remarks:
diff --git a/test-suite/bugs/closed/shouldfail/2251.v b/test-suite/bugs/closed/shouldfail/2251.v
index 642717f4a..d0fa3f2b3 100644
--- a/test-suite/bugs/closed/shouldfail/2251.v
+++ b/test-suite/bugs/closed/shouldfail/2251.v
@@ -2,4 +2,5 @@
 
 Lemma evar_rewrite : (forall a : nat, a = 0 -> True) -> True.
 intros; eapply H.  (* goal is  ?30 = nil  *)
-rewrite plus_n_Sm.
+Fail rewrite plus_n_Sm.
+Abort.
diff --git a/test-suite/bugs/closed/shouldfail/2406.v b/test-suite/bugs/closed/shouldfail/2406.v
index 112ea2bbf..d46fbabbb 100644
--- a/test-suite/bugs/closed/shouldfail/2406.v
+++ b/test-suite/bugs/closed/shouldfail/2406.v
@@ -1,3 +1,3 @@
 (* Check correct handling of unsupported notations *)
 Notation "'’'" := (fun x => x) (at level 20).
-Definition crash_the_rooster f := ’.
+Fail Definition crash_the_rooster f := ’.
diff --git a/test-suite/bugs/closed/shouldfail/2586.v b/test-suite/bugs/closed/shouldfail/2586.v
index 6111a6415..7e02e7f11 100644
--- a/test-suite/bugs/closed/shouldfail/2586.v
+++ b/test-suite/bugs/closed/shouldfail/2586.v
@@ -2,4 +2,5 @@ Require Import Setoid SetoidClass Program.
 
 Goal forall `(Setoid nat) x y, x == y -> S x == S y.
   intros.
-  clsubst H0.
\ No newline at end of file
+  Fail clsubst H0.
+  Abort.
\ No newline at end of file