test-suite: cleaning

12 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_106.v b/test-suite/bugs/opened/HoTT_coq_106.v
index a566459546..5873ba6c5d 100644
--- a/test-suite/bugs/opened/HoTT_coq_106.v
+++ b/test-suite/bugs/opened/HoTT_coq_106.v
@@ -50,3 +50,4 @@ UNDEFINED UNIVERSES:
  Top.32
  Top.33CONSTRAINTS:[] [A H B] |- ?13 == ?12
 [] [A H B H0] |- ?12 == ?15 *)
+Abort.
diff --git a/test-suite/bugs/opened/bug_3277.v b/test-suite/bugs/opened/bug_3277.v
index 5f4231363a..54629d8511 100644
--- a/test-suite/bugs/opened/bug_3277.v
+++ b/test-suite/bugs/opened/bug_3277.v
@@ -5,3 +5,4 @@ Goal True.
 Admitted.
 Goal True.
   Fail exact ltac:(evarr _). (* Error: Cannot infer this placeholder. *)
+Abort.
diff --git a/test-suite/bugs/opened/bug_3311.v b/test-suite/bugs/opened/bug_3311.v
index 1c66bc1e55..23752acf1c 100644
--- a/test-suite/bugs/opened/bug_3311.v
+++ b/test-suite/bugs/opened/bug_3311.v
@@ -8,3 +8,4 @@ Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraint
 Could not find an instance for "subrelation eq (Basics.flip Basics.impl)".
 With the following constraints:
 ?3 : "True" *)
+Abort.
diff --git a/test-suite/bugs/opened/bug_3312.v b/test-suite/bugs/opened/bug_3312.v
index 749921e2f6..bf87c3995f 100644
--- a/test-suite/bugs/opened/bug_3312.v
+++ b/test-suite/bugs/opened/bug_3312.v
@@ -3,3 +3,4 @@ Axiom bar : 0 = 1.
 Goal 0 = 1.
   Fail rewrite_strat bar. (* Toplevel input, characters 15-32:
 Error: Tactic failure:setoid rewrite failed: Nothing to rewrite. *)
+Abort.
diff --git a/test-suite/bugs/opened/bug_3343.v b/test-suite/bugs/opened/bug_3343.v
index 6c5a85f9cf..7c0470bf96 100644
--- a/test-suite/bugs/opened/bug_3343.v
+++ b/test-suite/bugs/opened/bug_3343.v
@@ -44,3 +44,4 @@ Proof.
   induction m.
   Fail progress simpl.
   (* simpl did nothing here, while it does something inside the section; this is probably a bug*)
+Abort.
diff --git a/test-suite/bugs/opened/bug_3345.v b/test-suite/bugs/opened/bug_3345.v
index 3e3da6df71..bc0f1a8604 100644
--- a/test-suite/bugs/opened/bug_3345.v
+++ b/test-suite/bugs/opened/bug_3345.v
@@ -143,3 +143,4 @@ cannot be applied to the terms
  "e0" : "nth_error Bound (ibound idx') = e"
 The 2nd term has type "nth_error Bound (ibound idx') = e"
 which should be coercible to "e = e". *)
+Abort.
diff --git a/test-suite/bugs/opened/bug_3370.v b/test-suite/bugs/opened/bug_3370.v
index 4964bf96c0..d6fc88a03a 100644
--- a/test-suite/bugs/opened/bug_3370.v
+++ b/test-suite/bugs/opened/bug_3370.v
@@ -10,3 +10,4 @@ Local Open Scope string_scope.
 Goal "asdf" = "bds".
 Fail set_strings. (* Error: Ltac variable s is bound to "asdf" which cannot be coerced to
 a fresh identifier. *)
+Abort.
diff --git a/test-suite/bugs/opened/bug_3395.v b/test-suite/bugs/opened/bug_3395.v
index 5ca48fc9d6..70b3a48a06 100644
--- a/test-suite/bugs/opened/bug_3395.v
+++ b/test-suite/bugs/opened/bug_3395.v
@@ -229,3 +229,4 @@ Proof.
   unfold yoneda; simpl in *.
   Fail Timeout 1 exact CYE.
   Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *)
+Abort.
diff --git a/test-suite/bugs/opened/bug_3463.v b/test-suite/bugs/opened/bug_3463.v
index 124f2bcc03..3de9e2ee5f 100644
--- a/test-suite/bugs/opened/bug_3463.v
+++ b/test-suite/bugs/opened/bug_3463.v
@@ -10,3 +10,4 @@ Goal True.
   test2 nat (1 + _).
   test3 (1 + _) nat.
   test3 (1 + _ : nat) nat.
+Abort.
diff --git a/test-suite/bugs/opened/bug_3655.v b/test-suite/bugs/opened/bug_3655.v
index 841f77febb..a9735be932 100644
--- a/test-suite/bugs/opened/bug_3655.v
+++ b/test-suite/bugs/opened/bug_3655.v
@@ -7,3 +7,4 @@ Goal True.
    guess it is still a bug in the sense that the semantics of pose is
    not preserved *)
   foo baz'.
+Abort.
diff --git a/test-suite/bugs/opened/bug_4755.v b/test-suite/bugs/opened/bug_4755.v
index 9cc0d361ea..50e40c5fad 100644
--- a/test-suite/bugs/opened/bug_4755.v
+++ b/test-suite/bugs/opened/bug_4755.v
@@ -32,3 +32,4 @@ Proof.
   intro.
   pose proof (_ : (Proper (_ ==> eq ==> _) and)).
   Fail setoid_rewrite (FG _ _); []. (* In 8.5: Error: Tactic failure: Incorrect number of goals (expected 2 tactics); works in 8.4 *)
+Abort.
diff --git a/test-suite/bugs/opened/bug_4778.v b/test-suite/bugs/opened/bug_4778.v
index 633d158e96..d66373ed7c 100644
--- a/test-suite/bugs/opened/bug_4778.v
+++ b/test-suite/bugs/opened/bug_4778.v
@@ -33,3 +33,4 @@ Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k.
   intro.
   pose proof (_ : (Proper (_ ==> eq ==> _) and)).
   Fail setoid_rewrite (FG _ _); [ | reflexivity.. ]. (* this should succeed without [Fail], as it does in 8.4 *)
+Abort.