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

66 files changed, 79 insertions, 77 deletions

diff --git a/test-suite/failure/Case1.v b/test-suite/failure/Case1.v
index df11ed386..6e76d42d2 100644
--- a/test-suite/failure/Case1.v
+++ b/test-suite/failure/Case1.v
@@ -1,4 +1,4 @@
-Type match 0 with
+Fail Type match 0 with
      | x => 0
      | O => 1
      end.
diff --git a/test-suite/failure/Case10.v b/test-suite/failure/Case10.v
index 43cc1e348..661d98cd5 100644
--- a/test-suite/failure/Case10.v
+++ b/test-suite/failure/Case10.v
@@ -1,3 +1,3 @@
-Type (fun x : nat => match x return nat with
+Fail Type (fun x : nat => match x return nat with
                      | S x as b => S b
                      end).
diff --git a/test-suite/failure/Case11.v b/test-suite/failure/Case11.v
index e76d06093..675f79e6e 100644
--- a/test-suite/failure/Case11.v
+++ b/test-suite/failure/Case11.v
@@ -1,3 +1,3 @@
-Type (fun x : nat => match x return nat with
+Fail Type (fun x : nat => match x return nat with
                      | S x as b => S b x
                      end).
diff --git a/test-suite/failure/Case12.v b/test-suite/failure/Case12.v
index cf6c20267..4a77f139c 100644
--- a/test-suite/failure/Case12.v
+++ b/test-suite/failure/Case12.v
@@ -1,5 +1,5 @@
 
-Type
+Fail Type
   (fun x : nat =>
    match x return nat with
    | S x as b => match x with
diff --git a/test-suite/failure/Case13.v b/test-suite/failure/Case13.v
index 994dfd205..5c0aa3e12 100644
--- a/test-suite/failure/Case13.v
+++ b/test-suite/failure/Case13.v
@@ -1,4 +1,4 @@
-Type
+Fail Type
   (fun x : nat =>
    match x return nat with
    | S x as b => match x with
diff --git a/test-suite/failure/Case14.v b/test-suite/failure/Case14.v
index ba0c51a15..29cae7645 100644
--- a/test-suite/failure/Case14.v
+++ b/test-suite/failure/Case14.v
@@ -3,7 +3,7 @@ Inductive List (A : Set) : Set :=
   | Cons : A -> List A -> List A.
 
 Definition NIL := Nil nat.
-Type match Nil nat return (List nat) with
+Fail Type match Nil nat return (List nat) with
      | NIL => NIL
      | _ => NIL
      end.
diff --git a/test-suite/failure/Case15.v b/test-suite/failure/Case15.v
index 18faaf5c9..ec08e6142 100644
--- a/test-suite/failure/Case15.v
+++ b/test-suite/failure/Case15.v
@@ -1,6 +1,6 @@
 (* Non exhaustive pattern-matching *)
 
-Check
+Fail Check
   (fun x =>
    match x, x with
    | O, S (S y) => true
diff --git a/test-suite/failure/Case16.v b/test-suite/failure/Case16.v
index 3739adae0..df15a4283 100644
--- a/test-suite/failure/Case16.v
+++ b/test-suite/failure/Case16.v
@@ -1,6 +1,6 @@
 (* Check for redundant clauses *)
 
-Check
+Fail Check
   (fun x =>
    match x, x with
    | O, S (S y) => true
diff --git a/test-suite/failure/Case2.v b/test-suite/failure/Case2.v
index 7d81ee81b..f8c95b1ec 100644
--- a/test-suite/failure/Case2.v
+++ b/test-suite/failure/Case2.v
@@ -4,7 +4,7 @@ Inductive IFExpr : Set :=
   | Fa : IFExpr
   | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr.
 
-Type
+Fail Type
   (fun F : IFExpr =>
    match F return Prop with
    | IfE (Var _) H I => True
diff --git a/test-suite/failure/Case3.v b/test-suite/failure/Case3.v
index ca450d5b3..eaafd41fa 100644
--- a/test-suite/failure/Case3.v
+++ b/test-suite/failure/Case3.v
@@ -2,7 +2,7 @@ Inductive List (A : Set) : Set :=
   | Nil : List A
   | Cons : A -> List A -> List A.
 
-Type
+Fail Type
   (fun l : List nat =>
    match l return nat with
    | Nil nat => 0
diff --git a/test-suite/failure/Case4.v b/test-suite/failure/Case4.v
index de63c3f79..4da7ef0cb 100644
--- a/test-suite/failure/Case4.v
+++ b/test-suite/failure/Case4.v
@@ -1,5 +1,5 @@
 
-Definition Berry (x y z : bool) :=
+Fail Definition Berry (x y z : bool) :=
   match x, y, z with
   | true, false, _ => 0
   | false, _, true => 1
diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v
index 494443f1c..70e5b9886 100644
--- a/test-suite/failure/Case5.v
+++ b/test-suite/failure/Case5.v
@@ -2,6 +2,6 @@ Inductive MS : Set :=
   | X : MS -> MS
   | Y : MS -> MS.
 
-Type (fun p : MS => match p return nat with
+Fail Type (fun p : MS => match p return nat with
                     | X x => 0
                     end).
diff --git a/test-suite/failure/Case6.v b/test-suite/failure/Case6.v
index fb8659bf8..cb7b7de0d 100644
--- a/test-suite/failure/Case6.v
+++ b/test-suite/failure/Case6.v
@@ -2,7 +2,7 @@ Inductive List (A : Set) : Set :=
   | Nil : List A
   | Cons : A -> List A -> List A.
 
-Type (match Nil nat return List nat with
+Fail Type (match Nil nat return List nat with
       | NIL   => NIL
       | (CONS _ _)  => NIL
       end).
diff --git a/test-suite/failure/Case7.v b/test-suite/failure/Case7.v
index 64453481a..e1fd7df06 100644
--- a/test-suite/failure/Case7.v
+++ b/test-suite/failure/Case7.v
@@ -9,7 +9,7 @@ Definition length1 (n : nat) (l : listn n) :=
   | _ => 0
   end.
 
-Type
+Fail Type
   (fun (n : nat) (l : listn n) =>
    match n return nat with
    | O => 0
diff --git a/test-suite/failure/Case8.v b/test-suite/failure/Case8.v
index feae29a7a..035629fef 100644
--- a/test-suite/failure/Case8.v
+++ b/test-suite/failure/Case8.v
@@ -2,7 +2,7 @@ Inductive List (A : Set) : Set :=
   | Nil : List A
   | Cons : A -> List A -> List A.
 
-Type match Nil nat return nat with
+Fail Type match Nil nat return nat with
      | b => b
      | Cons _ _ _ as d => d
      end.
diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v
index ec4852300..642f85d7b 100644
--- a/test-suite/failure/Case9.v
+++ b/test-suite/failure/Case9.v
@@ -1,10 +1,8 @@
 Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}.
-Type
+Fail Type
   match compare 0 0 return nat with
 
       (* k<i *) | left _ (left _ _) => 0
    (* k=i *) | left _ _ => 0
    (* k>i *) | right _ _ => 0
   end.
-
-  end.
diff --git a/test-suite/failure/ClearBody.v b/test-suite/failure/ClearBody.v
index 609d5b3b0..e321e59f5 100644
--- a/test-suite/failure/ClearBody.v
+++ b/test-suite/failure/ClearBody.v
@@ -5,4 +5,4 @@ Goal True.
 set (n := 0) in *.
 set (I := refl_equal 0) in *.
 change (n = 0) in (type of I).
-clearbody n.
+Fail clearbody n.
diff --git a/test-suite/failure/ImportedCoercion.v b/test-suite/failure/ImportedCoercion.v
index 0a69b8517..1cac69f4b 100644
--- a/test-suite/failure/ImportedCoercion.v
+++ b/test-suite/failure/ImportedCoercion.v
@@ -4,4 +4,4 @@ Require Import make_local.
 
 (* Local coercion must not be used *)
 
-Check (0 = true).
+Fail Check (0 = true).
diff --git a/test-suite/failure/Notations.v b/test-suite/failure/Notations.v
index 074e176aa..83459de37 100644
--- a/test-suite/failure/Notations.v
+++ b/test-suite/failure/Notations.v
@@ -3,5 +3,5 @@
 Notation "! A" := (forall i:nat, A) (at level 60).
 
 (* Should fail: no dynamic capture *)
-Check ! (i=i).
+Fail Check ! (i=i).
 
diff --git a/test-suite/failure/Reordering.v b/test-suite/failure/Reordering.v
index 7b36d1c35..e79b20737 100644
--- a/test-suite/failure/Reordering.v
+++ b/test-suite/failure/Reordering.v
@@ -2,4 +2,4 @@
 
 Goal forall (A:Set) (x:A) (A':=A), True.
 intros.
-change ((fun (_:A') => Set) x) in (type of A).
+Fail change ((fun (_:A') => Set) x) in (type of A).
diff --git a/test-suite/failure/Sections.v b/test-suite/failure/Sections.v
index 9b3b35c13..928e214f4 100644
--- a/test-suite/failure/Sections.v
+++ b/test-suite/failure/Sections.v
@@ -1,4 +1,4 @@
 Module A.
 Section	B.
-End A.
-End A.
+Fail End A.
+(*End A.*)
diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
index cbe7473c0..80951b82a 100644
--- a/test-suite/failure/Tauto.v
+++ b/test-suite/failure/Tauto.v
@@ -17,4 +17,4 @@
 (* Fails because Tauto does not perform any Apply *)
 Goal (forall A : Prop, A \/ ~ A) -> forall x y : nat, x = y \/ x <> y.
 Proof.
-   tauto.
+   Fail tauto.
diff --git a/test-suite/failure/Uminus.v b/test-suite/failure/Uminus.v
index d96c1e8f9..cc31c7ae6 100644
--- a/test-suite/failure/Uminus.v
+++ b/test-suite/failure/Uminus.v
@@ -7,11 +7,11 @@ Inductive prop : Prop := down : Prop -> prop.
 (* Coq should reject the following access of a Prop buried inside
    a prop. *)
 
-Definition up (p:prop) : Prop := let (A) := p in A.
+Fail Definition up (p:prop) : Prop := let (A) := p in A.
 
 (* Otherwise, we would have a proof of False via Hurkens' paradox *)
 
-Definition paradox : False :=
+Fail Definition paradox : False :=
  Hurkens.NoRetractFromSmallPropositionToProp.paradox
    prop
    down
diff --git a/test-suite/failure/autorewritein.v b/test-suite/failure/autorewritein.v
index dc17742a7..191e035b3 100644
--- a/test-suite/failure/autorewritein.v
+++ b/test-suite/failure/autorewritein.v
@@ -9,7 +9,7 @@ Hint Rewrite Ack0 Ack1 Ack2 : base0.
 Lemma ResAck2 : forall H:(Ack 2 2 = 7 -> False), H=H  -> False.
 Proof.
   intros.
-  autorewrite with base0 in * using try (apply H1;reflexivity).
+  Fail autorewrite with base0 in * using try (apply H1;reflexivity).
 
 
 
diff --git a/test-suite/failure/cases.v b/test-suite/failure/cases.v
index 18faaf5c9..ec08e6142 100644
--- a/test-suite/failure/cases.v
+++ b/test-suite/failure/cases.v
@@ -1,6 +1,6 @@
 (* Non exhaustive pattern-matching *)
 
-Check
+Fail Check
   (fun x =>
    match x, x with
    | O, S (S y) => true
diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v
index 649fdd2dc..a148ebe8e 100644
--- a/test-suite/failure/check.v
+++ b/test-suite/failure/check.v
@@ -1,3 +1,3 @@
 Implicit Arguments eq [A].
 
-Check (bool = true).
+Fail Check (bool = true).
diff --git a/test-suite/failure/circular_subtyping1.v b/test-suite/failure/circular_subtyping1.v
index 0b3a8688e..e89539523 100644
--- a/test-suite/failure/circular_subtyping1.v
+++ b/test-suite/failure/circular_subtyping1.v
@@ -4,4 +4,4 @@ Module Type T. Declare Module M:S. End T.
 
 Module N:S. End N.
 Module NN <: T. Module M:=N. End NN.
-Module P <: T with Module M:=NN := NN.
+Fail Module P <: T with Module M:=NN := NN.
diff --git a/test-suite/failure/circular_subtyping2.v b/test-suite/failure/circular_subtyping2.v
index 3bacdc655..f6de884db 100644
--- a/test-suite/failure/circular_subtyping2.v
+++ b/test-suite/failure/circular_subtyping2.v
@@ -5,4 +5,4 @@ Module N:S. End N.
 
 Module F (X:S) (Y:T with Module M:=X). End F.
 
-Module G := F N N.
\ No newline at end of file
+Fail Module G := F N N.
\ No newline at end of file
diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v
index 25d3c165b..9c4596fcd 100644
--- a/test-suite/failure/clash_cons.v
+++ b/test-suite/failure/clash_cons.v
@@ -11,5 +11,5 @@
 Inductive X : Set :=
     cons : X.
 
-Inductive Y : Set :=
+Fail Inductive Y : Set :=
     cons : Y.
diff --git a/test-suite/failure/clashes.v b/test-suite/failure/clashes.v
index 207d62b95..1a59ec66d 100644
--- a/test-suite/failure/clashes.v
+++ b/test-suite/failure/clashes.v
@@ -5,5 +5,5 @@
 
 Section S.
 Variable n : nat.
-Inductive P : Set :=
+Fail Inductive P : Set :=
     n : P.
diff --git a/test-suite/failure/coqbugs0266.v b/test-suite/failure/coqbugs0266.v
index 79eef5c92..cc3f307a2 100644
--- a/test-suite/failure/coqbugs0266.v
+++ b/test-suite/failure/coqbugs0266.v
@@ -4,4 +4,4 @@ Section S.
 Let a := 0.
 Definition b := a.
 Goal b = b.
-clear a.
+Fail clear a.
diff --git a/test-suite/failure/evar1.v b/test-suite/failure/evar1.v
index 1a4e42a89..2b6fe7654 100644
--- a/test-suite/failure/evar1.v
+++ b/test-suite/failure/evar1.v
@@ -1,3 +1,3 @@
 (* This used to succeed by producing an ill-typed term in v8.2 *)
 
-Lemma u: forall A : Prop, (exist _ A A) = (exist _ A A).
+Fail Lemma u: forall A : Prop, (exist _ A A) = (exist _ A A).
diff --git a/test-suite/failure/evarclear1.v b/test-suite/failure/evarclear1.v
index 2e9fa0f35..60adadef4 100644
--- a/test-suite/failure/evarclear1.v
+++ b/test-suite/failure/evarclear1.v
@@ -6,5 +6,5 @@ eexists.
 unfold z.
 clear y z.
 (* should fail because the evar should no longer be allowed to depend on z *)
-instantiate (1:=z).
+Fail instantiate (1:=z).
 
diff --git a/test-suite/failure/evarclear2.v b/test-suite/failure/evarclear2.v
index e606a06f1..0f7768112 100644
--- a/test-suite/failure/evarclear2.v
+++ b/test-suite/failure/evarclear2.v
@@ -6,4 +6,4 @@ eexists.
 rename y into z.
 unfold z at 1 2.
 (* should fail because the evar type depends on z *)
-clear z.
+Fail clear z.
diff --git a/test-suite/failure/evarlemma.v b/test-suite/failure/evarlemma.v
index ea753e79c..ae40774c9 100644
--- a/test-suite/failure/evarlemma.v
+++ b/test-suite/failure/evarlemma.v
@@ -1,3 +1,3 @@
 (* Check success of inference of evars in the context of lemmas *)
 
-Lemma foo x : True.
+Fail Lemma foo x : True.
diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v
index 6abf6332d..556e420eb 100644
--- a/test-suite/failure/fixpoint1.v
+++ b/test-suite/failure/fixpoint1.v
@@ -5,6 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-Fixpoint PreParadox (u : unit) : False := PreParadox u.
-Definition Paradox := PreParadox tt.
+Fail Fixpoint PreParadox (u : unit) : False := PreParadox u.
+(*Definition Paradox := PreParadox tt.*)
 
diff --git a/test-suite/failure/fixpoint2.v b/test-suite/failure/fixpoint2.v
index d2f02ea13..7f11a99b1 100644
--- a/test-suite/failure/fixpoint2.v
+++ b/test-suite/failure/fixpoint2.v
@@ -3,4 +3,4 @@
 Goal nat->nat.
 fix f 1.
 intro n; apply f; assumption.
-Guarded.
+Fail Guarded.
diff --git a/test-suite/failure/fixpoint3.v b/test-suite/failure/fixpoint3.v
index 42f06916b..7d1d3ee69 100644
--- a/test-suite/failure/fixpoint3.v
+++ b/test-suite/failure/fixpoint3.v
@@ -6,7 +6,7 @@ Inductive I : Prop :=
 
 Definition i0 := C (fun _ x => x).
 
-Definition Paradox : False :=
+Fail Definition Paradox : False :=
  (fix ni i : False :=
   match i with
   | C f => ni (f _ i)
diff --git a/test-suite/failure/fixpoint4.v b/test-suite/failure/fixpoint4.v
index fd9563738..bf6133f1c 100644
--- a/test-suite/failure/fixpoint4.v
+++ b/test-suite/failure/fixpoint4.v
@@ -8,7 +8,7 @@ Inductive IMP : Prop :=
 
 Definition i0 := (LIMP (fun _ => CIMP (fun _ x => x))).
 
-Definition Paradox : False :=
+Fail Definition Paradox : False :=
  (fix F y o {struct o} : False :=
   match y with
   | tt => fun f =>
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
index cd3c81f49..fe556cfd5 100644
--- a/test-suite/failure/guard.v
+++ b/test-suite/failure/guard.v
@@ -10,7 +10,7 @@ Fixpoint F (n:nat) : False := F (match F n with end).
 *)
 (* de Bruijn mix-up *)
 (* If accepted, Eval compute in f 0. loops *)
-Definition f :=
+Fail Definition f :=
   let f (f1 f2:nat->nat) := f1 in
   let _ := 0 in
   let _ := 0 in
diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v
index 6c14c2c3d..4446941eb 100644
--- a/test-suite/failure/illtype1.v
+++ b/test-suite/failure/illtype1.v
@@ -5,4 +5,4 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-Check (S S).
+Fail Check (S S).
diff --git a/test-suite/failure/inductive1.v b/test-suite/failure/inductive1.v
index 3b57d9198..7f42e7e16 100644
--- a/test-suite/failure/inductive1.v
+++ b/test-suite/failure/inductive1.v
@@ -1,4 +1,4 @@
 (* A check that sort-polymorphic product is not set too low *)
 
 Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
-Check (fun (A:Type) (B:Prop) => (prod A B : Prop)).
+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
index b77474be0..827c6f9fa 100644
--- a/test-suite/failure/inductive2.v
+++ b/test-suite/failure/inductive2.v
@@ -1,4 +1,4 @@
 (* A check that sort-polymorphic product is not set too low *)
 
 Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
-Check (fun (A:Prop) (B:Type) => (prod A B : Prop)).
+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
index cf035edf7..aacc9df71 100644
--- a/test-suite/failure/inductive3.v
+++ b/test-suite/failure/inductive3.v
@@ -2,4 +2,4 @@
    non uniform parameters (at least if these parameters break positivity) *)
 
 Inductive t (A:Type) : Type := c : t (A -> A) -> t A.
-Inductive u : Type := d : u | e : t u -> u.
+Fail Inductive u : Type := d : u | e : t u -> u.
diff --git a/test-suite/failure/inductive4.v b/test-suite/failure/inductive4.v
index 6ba36fd20..4563490dc 100644
--- a/test-suite/failure/inductive4.v
+++ b/test-suite/failure/inductive4.v
@@ -4,12 +4,12 @@ Require Import Logic.
 Require Hurkens.
 Definition Ti := Type.
 Inductive prod (X Y:Ti) := pair : X -> Y -> prod X Y.
-Definition B : Prop := let F := prod True in F Prop. (* Aie! *)
-Definition p2b (P:Prop) : B := pair True Prop I P.
+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.
+Check Hurkens.paradox B p2b b2p L1 L2.*)
 
diff --git a/test-suite/failure/ltac1.v b/test-suite/failure/ltac1.v
index 7b496a750..eef16525d 100644
--- a/test-suite/failure/ltac1.v
+++ b/test-suite/failure/ltac1.v
@@ -4,4 +4,4 @@ Ltac X := match goal with
           end.
 Goal True -> True -> True.
 intros.
-X.
+Fail X.
diff --git a/test-suite/failure/ltac2.v b/test-suite/failure/ltac2.v
index 14436e588..d66fb6808 100644
--- a/test-suite/failure/ltac2.v
+++ b/test-suite/failure/ltac2.v
@@ -1,6 +1,6 @@
 (* Check that Match arguments are forbidden *)
 Ltac E x := apply x.
 Goal True -> True.
-E ltac:(match goal with
+Fail E ltac:(match goal with
         |  |- _ => intro H
         end).
diff --git a/test-suite/failure/ltac4.v b/test-suite/failure/ltac4.v
index 414712754..5b0396d16 100644
--- a/test-suite/failure/ltac4.v
+++ b/test-suite/failure/ltac4.v
@@ -1,5 +1,6 @@
 (* Check static globalisation of tactic names *)
 (* Proposed by Benjamin (mars 2002) *)
 Goal forall n : nat, n = n.
-induction n; try REflexivity.
+induction n.
+Fail try REflexivity.
 
diff --git a/test-suite/failure/pattern.v b/test-suite/failure/pattern.v
index a24beaa2e..216eb254c 100644
--- a/test-suite/failure/pattern.v
+++ b/test-suite/failure/pattern.v
@@ -6,4 +6,4 @@ Variable P : forall m : nat, m = n -> Prop.
 
 Goal forall p : n = n, P n p.
 intro.
-pattern n, p.
+Fail pattern n, p.
diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v
index 03cc1109c..02557664a 100644
--- a/test-suite/failure/positivity.v
+++ b/test-suite/failure/positivity.v
@@ -5,5 +5,5 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-Inductive t : Set :=
+Fail Inductive t : Set :=
     c : (t -> nat) -> t.
diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v
index 93e159e8b..b62f9b686 100644
--- a/test-suite/failure/proofirrelevance.v
+++ b/test-suite/failure/proofirrelevance.v
@@ -6,6 +6,9 @@ Inductive bool_in_prop : Type := hide : bool -> bool_in_prop
 with bool : Type := true : bool | false : bool.
 
 Lemma not_proof_irrelevance : ~ forall (P:Prop) (p p':P), p=p'.
-intro H; pose proof (H bool_in_prop (hide true) (hide false)); discriminate.
-Qed.
+intro H.
+Fail pose proof (H bool_in_prop (hide true) (hide false)).
+Abort.
+(*discriminate.
+Qed.*)
 
diff --git a/test-suite/failure/prop-set-proof-irrelevance.v b/test-suite/failure/prop-set-proof-irrelevance.v
index ad4941084..fee33432b 100644
--- a/test-suite/failure/prop-set-proof-irrelevance.v
+++ b/test-suite/failure/prop-set-proof-irrelevance.v
@@ -1,12 +1,12 @@
 Require Import ProofIrrelevance.
 
 Lemma proof_irrelevance_set : forall (P : Set) (p1 p2 : P), p1 = p2.
-  exact proof_irrelevance.
-Qed.
+  Fail exact proof_irrelevance.
+(*Qed.
 
 Lemma paradox : False.
   assert (H : 0 <> 1) by discriminate.
   apply H.
   Fail apply proof_irrelevance. (* inlined version is rejected *)
   apply proof_irrelevance_set.
-Qed.
+Qed.*)
diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v
index 0c39b2761..5bf3e6d7e 100644
--- a/test-suite/failure/redef.v
+++ b/test-suite/failure/redef.v
@@ -6,4 +6,4 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 Definition toto := Set.
-Definition toto := Set.
+Fail Definition toto := Set.
diff --git a/test-suite/failure/rewrite_in_goal.v b/test-suite/failure/rewrite_in_goal.v
index c11a6237c..dedfdf01e 100644
--- a/test-suite/failure/rewrite_in_goal.v
+++ b/test-suite/failure/rewrite_in_goal.v
@@ -1,3 +1,3 @@
 Goal forall T1 T2 (H:T1=T2) (f:T1->Prop) (x:T1) , f x -> Type.
   intros until x.
-  rewrite H in x.
+  Fail rewrite H in x.
diff --git a/test-suite/failure/rewrite_in_hyp.v b/test-suite/failure/rewrite_in_hyp.v
index 613d707c6..1eef0fa03 100644
--- a/test-suite/failure/rewrite_in_hyp.v
+++ b/test-suite/failure/rewrite_in_hyp.v
@@ -1,3 +1,3 @@
 Goal forall (T1 T2 : Type) (f:T1 -> Prop) (x:T1) (H:T1=T2), f x -> 0=1.
   intros T1 T2 f x H fx.
-  rewrite H in x.
+  Fail rewrite H in x.
diff --git a/test-suite/failure/rewrite_in_hyp2.v b/test-suite/failure/rewrite_in_hyp2.v
index 1533966ef..112a856e3 100644
--- a/test-suite/failure/rewrite_in_hyp2.v
+++ b/test-suite/failure/rewrite_in_hyp2.v
@@ -5,4 +5,4 @@
 
 Goal forall b, S b = O -> (fun a => 0 = (S a)) b -> True.
   intros b H H0.
-  rewrite H in H0.
+  Fail rewrite H in H0.
diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v
index 38a627660..aa814f33d 100644
--- a/test-suite/failure/search.v
+++ b/test-suite/failure/search.v
@@ -6,4 +6,4 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-SearchPattern (_ = _) outside n_existe_pas.
+Fail SearchPattern (_ = _) outside n_existe_pas.
diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v
index 127da8513..e48c66891 100644
--- a/test-suite/failure/subtyping.v
+++ b/test-suite/failure/subtyping.v
@@ -18,4 +18,4 @@ Module TT : T.
  | L0
  | L1 :  (A -> Prop) -> L.
 
-End TT.
+Fail End TT.
diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v
index 48fc2fffa..8b2dc1dc6 100644
--- a/test-suite/failure/subtyping2.v
+++ b/test-suite/failure/subtyping2.v
@@ -242,4 +242,4 @@ Defined.
    with the constraint j >= i in the paradox.
 *)
 
-  Definition Paradox : False := Burali_Forti A0 i0' inj.
+  Fail Definition Paradox : False := Burali_Forti A0 i0' inj.
diff --git a/test-suite/failure/univ_include.v b/test-suite/failure/univ_include.v
index 56f04f9d6..28a3263d3 100644
--- a/test-suite/failure/univ_include.v
+++ b/test-suite/failure/univ_include.v
@@ -23,8 +23,8 @@ Module Mt.
   Definition t := T.
 End Mt.
 
-Module P := G Mt. (* should yield Universe inconsistency *)
+Fail Module P := G Mt. (* should yield Universe inconsistency *)
 (* ... otherwise the following command will show that T has type T! *)
-Eval cbv delta [P.elt Mt.t] in P.elt.
+(* Eval cbv delta [P.elt Mt.t] in P.elt. *)
 
 
diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v
index c101339a6..e01681588 100644
--- a/test-suite/failure/universes-buraliforti-redef.v
+++ b/test-suite/failure/universes-buraliforti-redef.v
@@ -243,4 +243,4 @@ Defined.
    with the constraint j >= i in the paradox.
 *)
 
-  Definition Paradox : False := Burali_Forti A0 i0 inj.
+  Fail Definition Paradox : False := Burali_Forti A0 i0 inj.
diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v
index 7b62a0c56..dba1a794f 100644
--- a/test-suite/failure/universes-buraliforti.v
+++ b/test-suite/failure/universes-buraliforti.v
@@ -234,4 +234,4 @@ Defined.
    with the constraint j >= i in the paradox.
 *)
 
-  Definition Paradox : False := Burali_Forti A0 i0 inj.
+  Fail Definition Paradox : False := Burali_Forti A0 i0 inj.
diff --git a/test-suite/failure/universes-sections1.v b/test-suite/failure/universes-sections1.v
index 6cd043492..3f8e44462 100644
--- a/test-suite/failure/universes-sections1.v
+++ b/test-suite/failure/universes-sections1.v
@@ -5,4 +5,4 @@ Section A.
   Definition Type1 : Type2 := Type.
 End A.
 
-Definition Inconsistency : Type1 := Type2.
+Fail Definition Inconsistency : Type1 := Type2.
diff --git a/test-suite/failure/universes-sections2.v b/test-suite/failure/universes-sections2.v
index 98fdbc0d1..34b2a11de 100644
--- a/test-suite/failure/universes-sections2.v
+++ b/test-suite/failure/universes-sections2.v
@@ -7,4 +7,4 @@ Section A.
   Definition Type1' := Type1.
 End A.
 
-Definition Inconsistency : Type1' := Type2.
+Fail Definition Inconsistency : Type1' := Type2.
diff --git a/test-suite/failure/universes.v b/test-suite/failure/universes.v
index 938c29b83..d708b01ff 100644
--- a/test-suite/failure/universes.v
+++ b/test-suite/failure/universes.v
@@ -1,3 +1,3 @@
 Definition Type2 := Type.
 Definition Type1 : Type2 := Type.
-Definition Inconsistency : Type1 := Type2.
+Fail Definition Inconsistency : Type1 := Type2.
diff --git a/test-suite/failure/universes3.v b/test-suite/failure/universes3.v
index 8fb414d5a..ee7a63c84 100644
--- a/test-suite/failure/universes3.v
+++ b/test-suite/failure/universes3.v
@@ -17,7 +17,7 @@ Inductive I (B:Type (*6*)) := C : B -> impl Prop (I B).
 
 (* We cannot enforce Type1 < Type(6) while we already have
    Type(6) <= Type(7) < Type3 < Type1 *)
-Definition J := I Type1.
+Fail Definition J := I Type1.
 
 (* Open question: should the type of an inductive be the max of the
    types of the _arguments_ of its constructors (here B and Prop,