test-suite: cleaning

19 files changed, 27 insertions, 5 deletions

diff --git a/test-suite/failure/ClearBody.v b/test-suite/failure/ClearBody.v
index e321e59f58..e865f121e8 100644
--- a/test-suite/failure/ClearBody.v
+++ b/test-suite/failure/ClearBody.v
@@ -6,3 +6,4 @@ set (n := 0) in *.
 set (I := refl_equal 0) in *.
 change (n = 0) in (type of I).
 Fail clearbody n.
+Abort.
diff --git a/test-suite/failure/Reordering.v b/test-suite/failure/Reordering.v
index e79b20737b..75cf372b43 100644
--- a/test-suite/failure/Reordering.v
+++ b/test-suite/failure/Reordering.v
@@ -3,3 +3,4 @@
 Goal forall (A:Set) (x:A) (A':=A), True.
 intros.
 Fail change ((fun (_:A') => Set) x) in (type of A).
+Abort.
diff --git a/test-suite/failure/Sections.v b/test-suite/failure/Sections.v
index 928e214f47..815fadd8a5 100644
--- a/test-suite/failure/Sections.v
+++ b/test-suite/failure/Sections.v
@@ -2,3 +2,5 @@ Module A.
 Section	B.
 Fail End A.
 (*End A.*)
+End B.
+End A.
diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
index 81d5b6358e..c10cb0b869 100644
--- a/test-suite/failure/Tauto.v
+++ b/test-suite/failure/Tauto.v
@@ -20,3 +20,4 @@
 Goal (forall A : Prop, A \/ ~ A) -> forall x y : nat, x = y \/ x <> y.
 Proof.
    Fail tauto.
+Abort.
diff --git a/test-suite/failure/autorewritein.v b/test-suite/failure/autorewritein.v
index 191e035b3a..b734d85933 100644
--- a/test-suite/failure/autorewritein.v
+++ b/test-suite/failure/autorewritein.v
@@ -10,6 +10,4 @@ Lemma ResAck2 : forall H:(Ack 2 2 = 7 -> False), H=H  -> False.
 Proof.
   intros.
   Fail autorewrite with base0 in * using try (apply H1;reflexivity).
-
-
-
+Abort.
diff --git a/test-suite/failure/clashes.v b/test-suite/failure/clashes.v
index 1a59ec66d1..1abec329c4 100644
--- a/test-suite/failure/clashes.v
+++ b/test-suite/failure/clashes.v
@@ -7,3 +7,4 @@ Section S.
 Variable n : nat.
 Fail Inductive P : Set :=
     n : P.
+End S.
diff --git a/test-suite/failure/coqbugs0266.v b/test-suite/failure/coqbugs0266.v
index cc3f307a20..79ea5ede47 100644
--- a/test-suite/failure/coqbugs0266.v
+++ b/test-suite/failure/coqbugs0266.v
@@ -5,3 +5,5 @@ Let a := 0.
 Definition b := a.
 Goal b = b.
 Fail clear a.
+Abort.
+End S.
diff --git a/test-suite/failure/evarclear1.v b/test-suite/failure/evarclear1.v
index 60adadef40..82697bf41e 100644
--- a/test-suite/failure/evarclear1.v
+++ b/test-suite/failure/evarclear1.v
@@ -7,4 +7,4 @@ unfold z.
 clear y z.
 (* should fail because the evar should no longer be allowed to depend on z *)
 Fail instantiate (1:=z).
-
+Abort.
diff --git a/test-suite/failure/evarclear2.v b/test-suite/failure/evarclear2.v
index 0f7768112b..45eeef6aa7 100644
--- a/test-suite/failure/evarclear2.v
+++ b/test-suite/failure/evarclear2.v
@@ -7,3 +7,4 @@ rename y into z.
 unfold z at 1 2.
 (* should fail because the evar type depends on z *)
 Fail clear z.
+Abort.
diff --git a/test-suite/failure/fixpoint2.v b/test-suite/failure/fixpoint2.v
index 7f11a99b16..2d2d6a02cd 100644
--- a/test-suite/failure/fixpoint2.v
+++ b/test-suite/failure/fixpoint2.v
@@ -4,3 +4,4 @@ Goal nat->nat.
 fix f 1.
 intro n; apply f; assumption.
 Fail Guarded.
+Abort.
diff --git a/test-suite/failure/ltac1.v b/test-suite/failure/ltac1.v
index eef16525d6..1cd119f3eb 100644
--- a/test-suite/failure/ltac1.v
+++ b/test-suite/failure/ltac1.v
@@ -5,3 +5,4 @@ Ltac X := match goal with
 Goal True -> True -> True.
 intros.
 Fail X.
+Abort.
diff --git a/test-suite/failure/ltac2.v b/test-suite/failure/ltac2.v
index d66fb6808d..8a9157df84 100644
--- a/test-suite/failure/ltac2.v
+++ b/test-suite/failure/ltac2.v
@@ -4,3 +4,4 @@ Goal True -> True.
 Fail E ltac:(match goal with
         |  |- _ => intro H
         end).
+Abort.
diff --git a/test-suite/failure/ltac4.v b/test-suite/failure/ltac4.v
index 5b0396d164..58b791eb38 100644
--- a/test-suite/failure/ltac4.v
+++ b/test-suite/failure/ltac4.v
@@ -3,4 +3,4 @@
 Goal forall n : nat, n = n.
 induction n.
 Fail try REflexivity.
-
+Abort.
diff --git a/test-suite/failure/pattern.v b/test-suite/failure/pattern.v
index 216eb254c1..480f579502 100644
--- a/test-suite/failure/pattern.v
+++ b/test-suite/failure/pattern.v
@@ -7,3 +7,4 @@ Variable P : forall m : nat, m = n -> Prop.
 Goal forall p : n = n, P n p.
 intro.
 Fail pattern n, p.
+Abort.
diff --git a/test-suite/failure/prop_set_proof_irrelevance.v b/test-suite/failure/prop_set_proof_irrelevance.v
index fee33432b0..ed6d4300e0 100644
--- a/test-suite/failure/prop_set_proof_irrelevance.v
+++ b/test-suite/failure/prop_set_proof_irrelevance.v
@@ -10,3 +10,4 @@ Lemma paradox : False.
   Fail apply proof_irrelevance. (* inlined version is rejected *)
   apply proof_irrelevance_set.
 Qed.*)
+Abort.
diff --git a/test-suite/failure/rewrite_in_goal.v b/test-suite/failure/rewrite_in_goal.v
index dedfdf01eb..e7823f1cb1 100644
--- a/test-suite/failure/rewrite_in_goal.v
+++ b/test-suite/failure/rewrite_in_goal.v
@@ -1,3 +1,4 @@
 Goal forall T1 T2 (H:T1=T2) (f:T1->Prop) (x:T1) , f x -> Type.
   intros until x.
   Fail rewrite H in x.
+Abort.
diff --git a/test-suite/failure/rewrite_in_hyp.v b/test-suite/failure/rewrite_in_hyp.v
index 1eef0fa033..f1b2203acc 100644
--- a/test-suite/failure/rewrite_in_hyp.v
+++ b/test-suite/failure/rewrite_in_hyp.v
@@ -1,3 +1,4 @@
 Goal forall (T1 T2 : Type) (f:T1 -> Prop) (x:T1) (H:T1=T2), f x -> 0=1.
   intros T1 T2 f x H fx.
   Fail rewrite H in x.
+Abort.
diff --git a/test-suite/failure/rewrite_in_hyp2.v b/test-suite/failure/rewrite_in_hyp2.v
index 112a856e32..60994fe1ed 100644
--- a/test-suite/failure/rewrite_in_hyp2.v
+++ b/test-suite/failure/rewrite_in_hyp2.v
@@ -6,3 +6,4 @@
 Goal forall b, S b = O -> (fun a => 0 = (S a)) b -> True.
   intros b H H0.
   Fail rewrite H in H0.
+Abort.
diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v
index e48c668916..6996f4232a 100644
--- a/test-suite/failure/subtyping.v
+++ b/test-suite/failure/subtyping.v
@@ -19,3 +19,10 @@ Module TT : T.
  | L1 :  (A -> Prop) -> L.
 
 Fail End TT.
+
+ Reset L.
+ Inductive L : Prop :=
+ | L0
+ | L1 :  (A -> Prop) -> L.
+
+End TT.