test-suite: cleaning

294 files changed, 394 insertions, 27 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index bde0bfc91f..e35393b5e8 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -60,7 +60,6 @@ SINGLE_QUOTE="
 # wrap the arguments in parens, but only if they exist
 get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1)))))
 # get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop
-has_compile_flag = $(filter "-compile",$(call get_coq_prog_args,$(1)))
 has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1)))
 get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqtopcompile),$(coqtopload))
 
@@ -308,7 +307,7 @@ ssr: $(wildcard ssr/*.v:%.v=%.v.log)
 $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
-	  opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
+	  opts="$(if $(findstring modules/,$<),-R modules Mods)"; \
 	  echo $(call log_intro,$<); \
 	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
diff --git a/test-suite/bugs/closed/HoTT_coq_002.v b/test-suite/bugs/closed/HoTT_coq_002.v
index dba4d5998f..fbafc97580 100644
--- a/test-suite/bugs/closed/HoTT_coq_002.v
+++ b/test-suite/bugs/closed/HoTT_coq_002.v
@@ -31,3 +31,4 @@ F : @SpecializedFunctor (* Top.516 *) objC C
 The term "F" has type "@SpecializedFunctor (* Top.516 *) objC C"
  while it is expected to have type
  "@SpecializedFunctor (* Top.519 Top.520 *) objC C". *)
+End FunctorInterface.
diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v
index 5c45036643..35f8701b2f 100644
--- a/test-suite/bugs/closed/HoTT_coq_014.v
+++ b/test-suite/bugs/closed/HoTT_coq_014.v
@@ -200,3 +200,4 @@ Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (
   Morphism (FunctorCategory GraphIndexingCategory TypeCat) (UnderlyingGraph C) (UnderlyingGraph D). (* Anomaly: apply_coercion. Please report.*)
 Proof.
 Admitted.
+End test.
diff --git a/test-suite/bugs/closed/HoTT_coq_028.v b/test-suite/bugs/closed/HoTT_coq_028.v
index b03241402f..99bde6d7c0 100644
--- a/test-suite/bugs/closed/HoTT_coq_028.v
+++ b/test-suite/bugs/closed/HoTT_coq_028.v
@@ -12,3 +12,4 @@ Error: Cannot instantiate metavariable P of type
  match eq_sym e in (_ = y) return (T (f y) (f x)) with
  | eq_refl => m (f x)
  end = m (f x)" of incompatible type "forall x : O, x = x -> Prop". *)
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_042.v b/test-suite/bugs/closed/HoTT_coq_042.v
index 432cf7054f..e2eedd16e3 100644
--- a/test-suite/bugs/closed/HoTT_coq_042.v
+++ b/test-suite/bugs/closed/HoTT_coq_042.v
@@ -26,3 +26,4 @@ Let SetCatFoo' : Foo.
 (* Toplevel input, characters 15-20:
 Error: Universe inconsistency (cannot enforce Set <= Prop).
  *)
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_044.v b/test-suite/bugs/closed/HoTT_coq_044.v
index c824f53ba8..78b675eab9 100644
--- a/test-suite/bugs/closed/HoTT_coq_044.v
+++ b/test-suite/bugs/closed/HoTT_coq_044.v
@@ -33,3 +33,4 @@ r2 : Row (* Top.56 Top.57 *) Ts
 The term "Row (* Coq.Init.Logic.8 Top.59 *) Ts" has type
  "Type (* max(Top.58+1, Top.59) *)" while it is expected to have type
  "Type (* Coq.Init.Logic.8 *)" (Universe inconsistency). *)
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_047.v b/test-suite/bugs/closed/HoTT_coq_047.v
index bef3c33ca1..219689f9fc 100644
--- a/test-suite/bugs/closed/HoTT_coq_047.v
+++ b/test-suite/bugs/closed/HoTT_coq_047.v
@@ -46,3 +46,4 @@ Proof.
     destruct n0.
      destruct cr.
 (* Anomaly: Evar ?nnn was not declared. Please report. *)
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_049.v b/test-suite/bugs/closed/HoTT_coq_049.v
index 906ec329e0..31e7861de4 100644
--- a/test-suite/bugs/closed/HoTT_coq_049.v
+++ b/test-suite/bugs/closed/HoTT_coq_049.v
@@ -4,3 +4,4 @@ Goal forall y, @f_equal = y.
 intro.
 apply functional_extensionality_dep.
 (* Error: Ill-typed evar instance in HoTT/coq, Anomaly: Uncaught exception Reductionops.NotASort(_). Please report. before that. *)
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_057.v b/test-suite/bugs/closed/HoTT_coq_057.v
index e72ce0c5ec..1405232b8e 100644
--- a/test-suite/bugs/closed/HoTT_coq_057.v
+++ b/test-suite/bugs/closed/HoTT_coq_057.v
@@ -31,3 +31,4 @@ Proof.
   Set Printing Universes.
   try (apply IHsub in X). (* Toplevel input, characters 5-21:
 Error: Universe inconsistency (cannot enforce Top.47 = Set). *)
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_058.v b/test-suite/bugs/closed/HoTT_coq_058.v
index 3d16e7ac0d..09e4365ebe 100644
--- a/test-suite/bugs/closed/HoTT_coq_058.v
+++ b/test-suite/bugs/closed/HoTT_coq_058.v
@@ -139,3 +139,4 @@ let T1 := lazymatch type of F with (?T -> _) -> _ => constr:(T) end in
       rewrite transport_path_prod'_beta'.
       (* Anomaly: Uncaught exception Invalid_argument("to_constraints: non-trivial algebraic constraint between universes", _).
 Please report. *)
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_059.v b/test-suite/bugs/closed/HoTT_coq_059.v
index 2e6c735cf5..9800ba8e45 100644
--- a/test-suite/bugs/closed/HoTT_coq_059.v
+++ b/test-suite/bugs/closed/HoTT_coq_059.v
@@ -15,3 +15,4 @@ Section foo.
   (* Toplevel input, characters 0-60:
 Error: Universe inconsistency (cannot enforce Top.24 <= Top.23 because Top.23
 < Top.22 <= Top.24). *)
+End foo.
diff --git a/test-suite/bugs/closed/HoTT_coq_079.v b/test-suite/bugs/closed/HoTT_coq_079.v
index e70de9ca99..7e782139ea 100644
--- a/test-suite/bugs/closed/HoTT_coq_079.v
+++ b/test-suite/bugs/closed/HoTT_coq_079.v
@@ -14,3 +14,4 @@ Hint Resolve H : bar.
 Goal forall y : foo, @x y = @x y.
 intro y.
 progress auto with bar. (* failed to progress *)
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_083.v b/test-suite/bugs/closed/HoTT_coq_083.v
index 494b25c7b1..02c4b22a4d 100644
--- a/test-suite/bugs/closed/HoTT_coq_083.v
+++ b/test-suite/bugs/closed/HoTT_coq_083.v
@@ -27,3 +27,4 @@ generalize dependent (@ob C).
 intros T t.
 (* Toplevel input, characters 9-10:
 Error: No product even after head-reduction. *)
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_099.v b/test-suite/bugs/closed/HoTT_coq_099.v
index cd5b0c8ff6..a9119052cb 100644
--- a/test-suite/bugs/closed/HoTT_coq_099.v
+++ b/test-suite/bugs/closed/HoTT_coq_099.v
@@ -60,3 +60,4 @@ Top.168 <= Coq.Init.Datatypes.28
 Top.169 <= Coq.Init.Datatypes.29
 Top.169 <= Coq.Init.Datatypes.28
  (maybe a bugged tactic). *)
+End PreMonoidalCategory.
diff --git a/test-suite/bugs/closed/HoTT_coq_100.v b/test-suite/bugs/closed/HoTT_coq_100.v
index 663b6280e4..660283116d 100644
--- a/test-suite/bugs/closed/HoTT_coq_100.v
+++ b/test-suite/bugs/closed/HoTT_coq_100.v
@@ -150,3 +150,4 @@ cannot be applied to the terms
         Top.313 Top.314 Top.306 Top.316 Top.305 *)"
 The 4th term has type "Category (* Top.300 Set *) unit"
 which should be coercible to "Category (* Top.300 Top.307 *) unit". *)
+End CommaCategoryProjectionFunctor.
diff --git a/test-suite/bugs/closed/HoTT_coq_101.v b/test-suite/bugs/closed/HoTT_coq_101.v
index 3ef56892be..777fd8600a 100644
--- a/test-suite/bugs/closed/HoTT_coq_101.v
+++ b/test-suite/bugs/closed/HoTT_coq_101.v
@@ -76,3 +76,4 @@ Section FullyFaithful.
   Check @FunctorProduct' C TypeCatC YC. (* Toplevel input, characters 0-37:
 Error: Universe inconsistency. Cannot enforce Top.187 = Top.186 because
 Top.186 <= Top.189 < Top.191 <= Top.187). *)
+End FullyFaithful.
diff --git a/test-suite/bugs/closed/HoTT_coq_112.v b/test-suite/bugs/closed/HoTT_coq_112.v
index 5bee69fcde..c3ef2aa1a7 100644
--- a/test-suite/bugs/closed/HoTT_coq_112.v
+++ b/test-suite/bugs/closed/HoTT_coq_112.v
@@ -74,3 +74,4 @@ The 1st term has type "Univalence (* Top.934 Top.935 Top.936 Top.937 *)"
 which should be coercible to
  "Univalence (* Top.1003 Top.1003 Top.1001 Top.997 *)".
  *)
+End Univalence.
diff --git a/test-suite/bugs/closed/HoTT_coq_118.v b/test-suite/bugs/closed/HoTT_coq_118.v
index e41689cba3..37b6ff66a1 100644
--- a/test-suite/bugs/closed/HoTT_coq_118.v
+++ b/test-suite/bugs/closed/HoTT_coq_118.v
@@ -34,3 +34,4 @@ p : tt = tt
 
 ?46 : "Contr_internal (idpath = p)"
  *)
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v
index e46ea58bb3..a80d075f69 100644
--- a/test-suite/bugs/closed/HoTT_coq_120.v
+++ b/test-suite/bugs/closed/HoTT_coq_120.v
@@ -136,3 +136,5 @@ Section fully_faithful_helpers.
   Set Printing Universes.
   admit. (* Error: Universe inconsistency (cannot enforce Top.235 <= Set because Set
 < Top.235). *)
+  Abort.
+End fully_faithful_helpers.
diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v
index 7bed956f3e..f688f51222 100644
--- a/test-suite/bugs/closed/HoTT_coq_123.v
+++ b/test-suite/bugs/closed/HoTT_coq_123.v
@@ -174,3 +174,4 @@ Section FunctorSectionCategory.
               _);
     abstract (path_natural_transformation; admit).
   Defined. (* Stack overflow *)
+End FunctorSectionCategory.
diff --git a/test-suite/bugs/closed/bug_1341.v b/test-suite/bugs/closed/bug_1341.v
index 79a0a14d7c..9bdfffea3e 100644
--- a/test-suite/bugs/closed/bug_1341.v
+++ b/test-suite/bugs/closed/bug_1341.v
@@ -15,3 +15,5 @@ intros A B a b c f Hab Hbc.
 rewrite Hab.
 assumption.
 Qed.
+
+End Setoid_Bug.
diff --git a/test-suite/bugs/closed/bug_1414.v b/test-suite/bugs/closed/bug_1414.v
index ee9e2504a6..ab490fa315 100644
--- a/test-suite/bugs/closed/bug_1414.v
+++ b/test-suite/bugs/closed/bug_1414.v
@@ -38,3 +38,4 @@ Program Fixpoint union
             let (l1', r1') := split v2 u in
             join (union l1' l2 _ _ _ _) v2 (union (snd r1') r2 _ _ _ _)
   end.
+Reset union.
diff --git a/test-suite/bugs/closed/bug_1416.v b/test-suite/bugs/closed/bug_1416.v
index 667c6b1d5f..87ecce5c1d 100644
--- a/test-suite/bugs/closed/bug_1416.v
+++ b/test-suite/bugs/closed/bug_1416.v
@@ -27,3 +27,4 @@ Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
 Proof.
   intros Env A e p; eapply ex_intro.
   autorewrite with placeeq. (* Here is the bug *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_1501.v b/test-suite/bugs/closed/bug_1501.v
index e771e192dc..64eea68c37 100644
--- a/test-suite/bugs/closed/bug_1501.v
+++ b/test-suite/bugs/closed/bug_1501.v
@@ -65,3 +65,5 @@ Proof.
   setoid_rewrite H2.
   reflexivity.
 Qed.
+
+End Essais.
diff --git a/test-suite/bugs/closed/bug_1542.v b/test-suite/bugs/closed/bug_1542.v
index 52cfbbc496..1def7f4dba 100644
--- a/test-suite/bugs/closed/bug_1542.v
+++ b/test-suite/bugs/closed/bug_1542.v
@@ -38,3 +38,5 @@ intro; constructor 2.
   ^^^^^^^^^^^^^
 Error: Impossible to unify (seq.toto ?3 (seq.t.f2 ?3)) with
  (seq.toto a (t'.f2 a)).*)
+Abort.
+End koko.
diff --git a/test-suite/bugs/closed/bug_1545.v b/test-suite/bugs/closed/bug_1545.v
index 9ef796faf7..91ce4a76af 100644
--- a/test-suite/bugs/closed/bug_1545.v
+++ b/test-suite/bugs/closed/bug_1545.v
@@ -18,3 +18,5 @@ Module ti:=ta.t.
 Definition ex1:forall (c d:ti.X), (ta.a d)=(ta.a c) -> d=c.
 intros.
 injection H.
+Abort.
+End toto.
diff --git a/test-suite/bugs/closed/bug_1683.v b/test-suite/bugs/closed/bug_1683.v
index 802057fa8c..8ab030a297 100644
--- a/test-suite/bugs/closed/bug_1683.v
+++ b/test-suite/bugs/closed/bug_1683.v
@@ -37,3 +37,5 @@ rewrite foobar.
 rewrite foobar in H.
 assumption.
 Qed.
+
+End SetoidBug.
diff --git a/test-suite/bugs/closed/bug_1773.v b/test-suite/bugs/closed/bug_1773.v
index 211af89b70..c930f24df7 100644
--- a/test-suite/bugs/closed/bug_1773.v
+++ b/test-suite/bugs/closed/bug_1773.v
@@ -7,3 +7,4 @@ Proof.
   econstructor.
   intros X.
   apply X. (* used to fail here *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_1865.v b/test-suite/bugs/closed/bug_1865.v
index 17c1998948..8bbe07881c 100644
--- a/test-suite/bugs/closed/bug_1865.v
+++ b/test-suite/bugs/closed/bug_1865.v
@@ -16,3 +16,4 @@ Definition f (n:nat) : Type :=
 Goal forall A n, list A n -> f n.
 intros A n.
 dependent inversion n.
+Abort.
diff --git a/test-suite/bugs/closed/bug_1918.v b/test-suite/bugs/closed/bug_1918.v
index 9d92fe12b8..5d1f9edb3e 100644
--- a/test-suite/bugs/closed/bug_1918.v
+++ b/test-suite/bugs/closed/bug_1918.v
@@ -374,3 +374,4 @@ Proof.
 
 
 Abort.
+End BushDep.
diff --git a/test-suite/bugs/closed/bug_1944.v b/test-suite/bugs/closed/bug_1944.v
index ee2918c6e9..f996eeecc6 100644
--- a/test-suite/bugs/closed/bug_1944.v
+++ b/test-suite/bugs/closed/bug_1944.v
@@ -7,3 +7,4 @@ Lemma bug : forall n, J n -> J (S n).
 Proof.
   intros ? H.
   induction H as [? ? [? ?]].
+Abort.
diff --git a/test-suite/bugs/closed/bug_1963.v b/test-suite/bugs/closed/bug_1963.v
index 11e2ee44d6..354056ae2a 100644
--- a/test-suite/bugs/closed/bug_1963.v
+++ b/test-suite/bugs/closed/bug_1963.v
@@ -17,3 +17,4 @@ Lemma inv : forall (A:Type)(n n':nat)(ts':illist A n'), n' = S n ->
 Proof.
 intros.
 dependent inversion ts'.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2016.v b/test-suite/bugs/closed/bug_2016.v
index 927021a259..a82fd87986 100644
--- a/test-suite/bugs/closed/bug_2016.v
+++ b/test-suite/bugs/closed/bug_2016.v
@@ -62,3 +62,4 @@ apply sym_eq.
 Show Universes.
 Print Universes.
 Fail apply H0.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2117.v b/test-suite/bugs/closed/bug_2117.v
index 50c925617e..b68554a52a 100644
--- a/test-suite/bugs/closed/bug_2117.v
+++ b/test-suite/bugs/closed/bug_2117.v
@@ -54,3 +54,4 @@ Subst.
 apply copyf_atom.
 Show Existentials.
 apply H1.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2123.v b/test-suite/bugs/closed/bug_2123.v
index 2957e53e3c..0ff8bda6dc 100644
--- a/test-suite/bugs/closed/bug_2123.v
+++ b/test-suite/bugs/closed/bug_2123.v
@@ -7,3 +7,4 @@ Parameter widen : forall (n : nat) (s : fset n), { x : fset (S n) | s=s }.
 Goal forall i, fset (S i).
 intro.
 refine (proj1_sig (widen i _)).
+Abort.
diff --git a/test-suite/bugs/closed/bug_2139.v b/test-suite/bugs/closed/bug_2139.v
index e2e4784965..07b94d540a 100644
--- a/test-suite/bugs/closed/bug_2139.v
+++ b/test-suite/bugs/closed/bug_2139.v
@@ -22,3 +22,4 @@ apply flip in H.
    type of (@flip _ _ _ _) itself had non-normalized evars *)
 
 (* By the way, is the check necessary ? *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_2164.v b/test-suite/bugs/closed/bug_2164.v
index 6adb3577be..9119a02419 100644
--- a/test-suite/bugs/closed/bug_2164.v
+++ b/test-suite/bugs/closed/bug_2164.v
@@ -332,3 +332,4 @@ exists lv''.
    [| |t' lv''' lv'''' rv''' ee'' ee_sub' H2 (H3_1,H3_2,H3_3) (H4_1,H4_2,H4_3,H4_4,H4_5) H5 (H6_1,H6_2)| | | |].
 (* Check that all names are the given ones: *)
 clear t' lv''' lv'''' rv''' ee'' ee_sub' H2 H3_1 H3_2 H3_3 H4_1 H4_2 H4_3 H4_4 H4_5 H5 H6_1 H6_2.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2243.v b/test-suite/bugs/closed/bug_2243.v
index 6d45c9a09e..65a4c15eff 100644
--- a/test-suite/bugs/closed/bug_2243.v
+++ b/test-suite/bugs/closed/bug_2243.v
@@ -7,3 +7,5 @@ Proof.
 destruct H.
 Undo.
 revert H; intro H; destruct H.
+Abort.
+End O.
diff --git a/test-suite/bugs/closed/bug_2244.v b/test-suite/bugs/closed/bug_2244.v
index d72c51f216..948251082c 100644
--- a/test-suite/bugs/closed/bug_2244.v
+++ b/test-suite/bugs/closed/bug_2244.v
@@ -17,3 +17,4 @@ Proof.
 
   (* still not compatible with 8.2 because an evar can be solved in
      two different ways and is left open *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_2255.v b/test-suite/bugs/closed/bug_2255.v
index ae5024fddd..7981dc1f20 100644
--- a/test-suite/bugs/closed/bug_2255.v
+++ b/test-suite/bugs/closed/bug_2255.v
@@ -19,3 +19,4 @@ n0 & Tuple n0 H0})
             (consT A F) (cons A x F X))), False.
 intros.
 injection H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2295.v b/test-suite/bugs/closed/bug_2295.v
index f5ca28dcaa..584edf19b9 100644
--- a/test-suite/bugs/closed/bug_2295.v
+++ b/test-suite/bugs/closed/bug_2295.v
@@ -9,3 +9,5 @@ Definition d' :=
   | true => or_introl _ (refl_equal true)
   | false => or_intror _ (refl_equal false)
   end).
+
+End sec.
diff --git a/test-suite/bugs/closed/bug_2299.v b/test-suite/bugs/closed/bug_2299.v
index c0552ca7b3..2f0aad90b6 100644
--- a/test-suite/bugs/closed/bug_2299.v
+++ b/test-suite/bugs/closed/bug_2299.v
@@ -11,3 +11,6 @@ Let unused := T tt.
 Goal T tt -> False.
  intro X.
  destruct X.
+Abort.
+
+End test.
diff --git a/test-suite/bugs/closed/bug_2320.v b/test-suite/bugs/closed/bug_2320.v
index 1616a29de6..8c9b1f5049 100644
--- a/test-suite/bugs/closed/bug_2320.v
+++ b/test-suite/bugs/closed/bug_2320.v
@@ -12,3 +12,4 @@ Lemma failure : forall (x : dummy 0), x = constr.
 Proof.
 intros x.
 refine (match x with constr => _ end).
+Abort.
diff --git a/test-suite/bugs/closed/bug_2350.v b/test-suite/bugs/closed/bug_2350.v
index e91f22e267..18c7ebda54 100644
--- a/test-suite/bugs/closed/bug_2350.v
+++ b/test-suite/bugs/closed/bug_2350.v
@@ -4,3 +4,4 @@
 Definition foo := forall n:nat, n=n.
 Definition bar : foo.
 refine (fix aux (n:nat) := _).
+Abort.
diff --git a/test-suite/bugs/closed/bug_2360.v b/test-suite/bugs/closed/bug_2360.v
index 9aea5f3615..1aed53c6ed 100644
--- a/test-suite/bugs/closed/bug_2360.v
+++ b/test-suite/bugs/closed/bug_2360.v
@@ -10,3 +10,4 @@ Definition some_value (etyp : nat -> Type) :  (Value etyp).
 Proof.
   intros.
   Fail apply Mk. (* Check that it does not raise an anomaly *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_2378.v b/test-suite/bugs/closed/bug_2378.v
index b9dd654057..a96a23ff40 100644
--- a/test-suite/bugs/closed/bug_2378.v
+++ b/test-suite/bugs/closed/bug_2378.v
@@ -608,3 +608,6 @@ Next Obligation.
 Qed.
 
 End Product.
+
+End TRANSFO.
+End TTS_TASM.
diff --git a/test-suite/bugs/closed/bug_2404.v b/test-suite/bugs/closed/bug_2404.v
index f6ec676014..c284a15651 100644
--- a/test-suite/bugs/closed/bug_2404.v
+++ b/test-suite/bugs/closed/bug_2404.v
@@ -44,3 +44,5 @@ Fixpoint exportRweak {a b} (aRWb : Rweak a b) (y : bName b) : option (bName a) :
     | None   => None
     end
   end.
+
+End Derived.
diff --git a/test-suite/bugs/closed/bug_2602.v b/test-suite/bugs/closed/bug_2602.v
index 29c8ac16b2..dd3551a7c3 100644
--- a/test-suite/bugs/closed/bug_2602.v
+++ b/test-suite/bugs/closed/bug_2602.v
@@ -6,3 +6,4 @@ match goal with
        | |- S a > 0 => idtac
      end
 end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2616.v b/test-suite/bugs/closed/bug_2616.v
index 0be5b6c2c5..fee91dab24 100644
--- a/test-suite/bugs/closed/bug_2616.v
+++ b/test-suite/bugs/closed/bug_2616.v
@@ -5,3 +5,4 @@ Goal
 Proof.
 intros.
 Fail rewrite IN in H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2729.v b/test-suite/bugs/closed/bug_2729.v
index c9d65c12c7..ff08bdc6bb 100644
--- a/test-suite/bugs/closed/bug_2729.v
+++ b/test-suite/bugs/closed/bug_2729.v
@@ -113,3 +113,4 @@ Lemma insertBaseConsLt {pu : PatchUniverse}
                      : insertBase p (Cons q rs) = Cons p (Cons q rs).
 Proof.
 vm_compute.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2817.v b/test-suite/bugs/closed/bug_2817.v
index 08dff99287..5125ce072f 100644
--- a/test-suite/bugs/closed/bug_2817.v
+++ b/test-suite/bugs/closed/bug_2817.v
@@ -7,3 +7,4 @@ False.
 
 intros.
 Fail apply H in H0. (* should fail without exhausting the stack *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_2828.v b/test-suite/bugs/closed/bug_2828.v
index 0b8abace22..36ac4605f4 100644
--- a/test-suite/bugs/closed/bug_2828.v
+++ b/test-suite/bugs/closed/bug_2828.v
@@ -2,3 +2,4 @@ Parameter A B : Type.
 Coercion POL (p : prod A B) := fst p.
 Goal forall x : prod A B, A.
   intro x. Fail exact x.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2834.v b/test-suite/bugs/closed/bug_2834.v
index 6015c53b8a..afa405b8dd 100644
--- a/test-suite/bugs/closed/bug_2834.v
+++ b/test-suite/bugs/closed/bug_2834.v
@@ -2,3 +2,4 @@
 
 Lemma eqType2Set (a b : Set) (H : @eq Type a b) : @eq Set a b.
 Fail subst.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2836.v b/test-suite/bugs/closed/bug_2836.v
index a948b75e27..a2755be7dd 100644
--- a/test-suite/bugs/closed/bug_2836.v
+++ b/test-suite/bugs/closed/bug_2836.v
@@ -37,3 +37,5 @@ Fail refine {|
       Compose' := (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd
 m2) (snd m1)))
     |}.
+Abort.
+End ProductCategory.
diff --git a/test-suite/bugs/closed/bug_2837.v b/test-suite/bugs/closed/bug_2837.v
index 52a56c2cff..9982b96f79 100644
--- a/test-suite/bugs/closed/bug_2837.v
+++ b/test-suite/bugs/closed/bug_2837.v
@@ -13,3 +13,4 @@ Fail (intros; rewrite test).
 
 (* III) a working variant: *)
 intros; rewrite (test n m).
+Abort.
diff --git a/test-suite/bugs/closed/bug_2839.v b/test-suite/bugs/closed/bug_2839.v
index e727e26061..7388555a1f 100644
--- a/test-suite/bugs/closed/bug_2839.v
+++ b/test-suite/bugs/closed/bug_2839.v
@@ -8,3 +8,4 @@ Fail
     | [ H : context G [@eq _ _] |- _ ] => let H' := context G[@plus 2] in H'
     end
   in pose H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2854.v b/test-suite/bugs/closed/bug_2854.v
index 14aee17ff0..6bc102f569 100644
--- a/test-suite/bugs/closed/bug_2854.v
+++ b/test-suite/bugs/closed/bug_2854.v
@@ -5,3 +5,5 @@ Section foo.
     subst foo.
     Fail pose bar as f.
     (* simpl in f. *)
+  Abort.
+End foo.
diff --git a/test-suite/bugs/closed/bug_2883.v b/test-suite/bugs/closed/bug_2883.v
index f027b5eb29..9170ce41ca 100644
--- a/test-suite/bugs/closed/bug_2883.v
+++ b/test-suite/bugs/closed/bug_2883.v
@@ -33,3 +33,5 @@ Proof.
   eapply IHstar; eauto.
   replace s2 with (State a' e b') by admit. eauto.
 Qed. (* Oups *)
+
+End Test.
diff --git a/test-suite/bugs/closed/bug_2900.v b/test-suite/bugs/closed/bug_2900.v
index 8f4264e910..93ea71848b 100644
--- a/test-suite/bugs/closed/bug_2900.v
+++ b/test-suite/bugs/closed/bug_2900.v
@@ -26,3 +26,4 @@ Proof.
   intros * E Hp.
   (* bug goes away if [revert E] is called explicitly *)
   dependent induction Hp.
+Abort.
diff --git a/test-suite/bugs/closed/bug_2946.v b/test-suite/bugs/closed/bug_2946.v
index c8b7255e7b..9c96ae021e 100644
--- a/test-suite/bugs/closed/bug_2946.v
+++ b/test-suite/bugs/closed/bug_2946.v
@@ -6,3 +6,5 @@ assert (pairE1 := let Exy := _ in (Ex_ y, E_y _) : Exy * Exy).
 
 (* FAIL *)
 assert (pairE2 := let Exy := _ in (Ex_ _, E_y x) : Exy * Exy).
+
+Abort.
diff --git a/test-suite/bugs/closed/bug_2995.v b/test-suite/bugs/closed/bug_2995.v
index b6c5b6df44..1a4d7e5040 100644
--- a/test-suite/bugs/closed/bug_2995.v
+++ b/test-suite/bugs/closed/bug_2995.v
@@ -7,3 +7,7 @@ Module Implementation <: Interface.
   Definition error: t := false.
 Fail End Implementation.
 (* A UserError here is expected, not an uncaught Not_found *)
+
+ Reset error.
+ Definition error := 0.
+End Implementation.
diff --git a/test-suite/bugs/closed/bug_2996.v b/test-suite/bugs/closed/bug_2996.v
index d5409289c5..6736db898d 100644
--- a/test-suite/bugs/closed/bug_2996.v
+++ b/test-suite/bugs/closed/bug_2996.v
@@ -29,3 +29,5 @@ Section x.
     set (T := False).
     Fail pose proof p as H.
   Abort.
+
+End x.
diff --git a/test-suite/bugs/closed/bug_3003.v b/test-suite/bugs/closed/bug_3003.v
index 2f8bcdae7a..2484605f54 100644
--- a/test-suite/bugs/closed/bug_3003.v
+++ b/test-suite/bugs/closed/bug_3003.v
@@ -10,3 +10,4 @@ Inductive G_Edge : G_Vertex -> G_Vertex -> Set := G_e : G_Edge G_v0 G_v1.
 Goal forall x1 : G_Edge G_v1 G_v1, @AddEdge _ G_Edge G_v1 _ _ (NoEdges _ _) x1 = NoEdges _ _.
 intro x1.
 try destruct x1. (* now raises a typing error *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3016.v b/test-suite/bugs/closed/bug_3016.v
index bd4f1dd805..d9fd685eae 100644
--- a/test-suite/bugs/closed/bug_3016.v
+++ b/test-suite/bugs/closed/bug_3016.v
@@ -2,3 +2,5 @@ Section foo.
   Variable C : Type.
   Goal True.
     change (eq (A := ?C) ?x ?y) with (eq).
+  Abort.
+End foo.
diff --git a/test-suite/bugs/closed/bug_3036.v b/test-suite/bugs/closed/bug_3036.v
index d60987a9e6..dff15d4e10 100644
--- a/test-suite/bugs/closed/bug_3036.v
+++ b/test-suite/bugs/closed/bug_3036.v
@@ -167,3 +167,5 @@ Section Stack.
   Proof.
     intros.
     try apply himp_ex_conc_trivial.
+  Abort.
+End Stack.
diff --git a/test-suite/bugs/closed/bug_3037.v b/test-suite/bugs/closed/bug_3037.v
index baa7eff549..40d1bfde53 100644
--- a/test-suite/bugs/closed/bug_3037.v
+++ b/test-suite/bugs/closed/bug_3037.v
@@ -9,3 +9,4 @@ Function f_R (a: nat) {wf (fun x y: nat => False)  a}:Prop:=
   end.
 (* Anomaly: File "plugins/funind/recdef.ml", line 916, characters 13-19: Assertion failed.
 Please report. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3045.v b/test-suite/bugs/closed/bug_3045.v
index b3c8bfecbc..90aa5ee9fd 100644
--- a/test-suite/bugs/closed/bug_3045.v
+++ b/test-suite/bugs/closed/bug_3045.v
@@ -32,3 +32,4 @@ refine match m with
    it should work, if destruct were able to do the good generalization
    in advance, before doing the "intros []". *)
 Fail destruct (@ReifiedMorphismSimplifyWithProof T s1 d0 d0' m1) as [ [] ? ].
+Abort.
diff --git a/test-suite/bugs/closed/bug_3068.v b/test-suite/bugs/closed/bug_3068.v
index 04072ae305..00d00b421e 100644
--- a/test-suite/bugs/closed/bug_3068.v
+++ b/test-suite/bugs/closed/bug_3068.v
@@ -62,3 +62,6 @@ Section Finite_nat_set.
     (* This was not part of the initial bug report; this is to check that
        the existential variable kept its name *)
     change (true = counted_def_nth fs2 i ?def).
+
+  Abort.
+End Finite_nat_set.
diff --git a/test-suite/bugs/closed/bug_3070.v b/test-suite/bugs/closed/bug_3070.v
index 7a8feca587..3ebfaa3131 100644
--- a/test-suite/bugs/closed/bug_3070.v
+++ b/test-suite/bugs/closed/bug_3070.v
@@ -4,3 +4,4 @@ Lemma foo (a1 a2 : Set) (b1 : a1 -> Prop)
       (Ha : a1 = a2) (c : a1) (d : b1 c) : True.
 Proof.
   subst.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3100.v b/test-suite/bugs/closed/bug_3100.v
index 6f35a74dc1..37e0cb7119 100644
--- a/test-suite/bugs/closed/bug_3100.v
+++ b/test-suite/bugs/closed/bug_3100.v
@@ -7,3 +7,4 @@ Fixpoint F (n : nat) (A : Type) : Type :=
 Goal forall A n, (forall (x : A) (e : x = x), F n (e = e)).
 intros A n.
 Fail change (forall x, F n (x = x)) with (F (S n)).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3199.v b/test-suite/bugs/closed/bug_3199.v
index 08bf62493d..d1bd9017c1 100644
--- a/test-suite/bugs/closed/bug_3199.v
+++ b/test-suite/bugs/closed/bug_3199.v
@@ -16,3 +16,4 @@ Defined.
 Goal True.
 pose (e := eq_refl (qux 0)); unfold qux in e.
 match type of e with context [eq_sym] => fail 1 | _ => idtac end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3210.v b/test-suite/bugs/closed/bug_3210.v
index bb673f38c2..b320c59d0f 100644
--- a/test-suite/bugs/closed/bug_3210.v
+++ b/test-suite/bugs/closed/bug_3210.v
@@ -20,3 +20,4 @@ match goal with |- I = I => idtac end. (* check form of the goal *)
 Undo 2.
 destruct x.
 match goal with |- I = I => idtac end. (* check form of the goal *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3228.v b/test-suite/bugs/closed/bug_3228.v
index 5d1a0ff88b..7c0eba6e71 100644
--- a/test-suite/bugs/closed/bug_3228.v
+++ b/test-suite/bugs/closed/bug_3228.v
@@ -5,3 +5,4 @@ Ltac bar x := exact x.
 Goal False -> False.
   intro x.
   Fail bar doesnotexist.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3251.v b/test-suite/bugs/closed/bug_3251.v
index d4ce050c57..ef279688aa 100644
--- a/test-suite/bugs/closed/bug_3251.v
+++ b/test-suite/bugs/closed/bug_3251.v
@@ -12,3 +12,4 @@ Undo.
 Ltac foo := idtac.
 (* Before 5b39c3535f7b3383d89d7b844537244a4e7c0eca, this would print out: *)
 (* Anomaly: Backtrack.backto to a state with no vcs_backup. Please report. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3257.v b/test-suite/bugs/closed/bug_3257.v
index d8aa6a0479..88e2e71911 100644
--- a/test-suite/bugs/closed/bug_3257.v
+++ b/test-suite/bugs/closed/bug_3257.v
@@ -3,3 +3,4 @@ Lemma foo A B (P : B -> Prop) :
   pointwise_relation _ impl (fun z => A -> P z) P.
 Proof.
   Fail reflexivity.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3258.v b/test-suite/bugs/closed/bug_3258.v
index b263c6baf4..946aff7d08 100644
--- a/test-suite/bugs/closed/bug_3258.v
+++ b/test-suite/bugs/closed/bug_3258.v
@@ -34,3 +34,4 @@ Proof.
   Undo.
   (* This failed with NotConvertible at some time *)
   setoid_rewrite (@remove_forall_eq' _ _ _).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3260.v b/test-suite/bugs/closed/bug_3260.v
index 9f0231d91b..f07f449b12 100644
--- a/test-suite/bugs/closed/bug_3260.v
+++ b/test-suite/bugs/closed/bug_3260.v
@@ -5,3 +5,4 @@ replace n with m at 2.
 lazymatch goal with
 |- n + m = m + m => idtac
 end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3262.v b/test-suite/bugs/closed/bug_3262.v
index 70bfde2990..41b2c92281 100644
--- a/test-suite/bugs/closed/bug_3262.v
+++ b/test-suite/bugs/closed/bug_3262.v
@@ -76,3 +76,5 @@ Section hlist.
              | hlist_eqv_cons l ls x y h1 h2 pf pf' =>
                _
            end).
+  Abort.
+End hlist.
diff --git a/test-suite/bugs/closed/bug_3284.v b/test-suite/bugs/closed/bug_3284.v
index 34cd09c6f4..854889e61e 100644
--- a/test-suite/bugs/closed/bug_3284.v
+++ b/test-suite/bugs/closed/bug_3284.v
@@ -21,3 +21,4 @@ Proof.
   intros A B C f g x H.
   specialize (H x).
   apply functional_extensionality_dep in H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3286.v b/test-suite/bugs/closed/bug_3286.v
index 701480fc83..360a304a47 100644
--- a/test-suite/bugs/closed/bug_3286.v
+++ b/test-suite/bugs/closed/bug_3286.v
@@ -39,3 +39,4 @@ Proof.
   let lem := constr:(@functional_extensionality_dep) in
   apply_under_binders_in lem H.
 (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3291.v b/test-suite/bugs/closed/bug_3291.v
index 4ea748c0fb..19586abbfe 100644
--- a/test-suite/bugs/closed/bug_3291.v
+++ b/test-suite/bugs/closed/bug_3291.v
@@ -7,3 +7,4 @@ rewrite -> eq. auto.
 Set Typeclasses Debug.
 Fail setoid_rewrite <- H. (* The command has indeed failed with message:
 => Stack overflow. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3297.v b/test-suite/bugs/closed/bug_3297.v
index 1cacb97ff3..da8390c475 100644
--- a/test-suite/bugs/closed/bug_3297.v
+++ b/test-suite/bugs/closed/bug_3297.v
@@ -10,3 +10,4 @@ Error: Abstracting over the term "n" leads to a term
   intro.
   clearbody H.
   subst. (* success *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3310.v b/test-suite/bugs/closed/bug_3310.v
index d6c31c6b41..339280b2f2 100644
--- a/test-suite/bugs/closed/bug_3310.v
+++ b/test-suite/bugs/closed/bug_3310.v
@@ -9,3 +9,4 @@ Lemma id_spec : forall A (s : stream A), id s = s.
 Proof.
 intros A s.
 Fail change (id s) with (cons (hd (id s)) (tl (id s))).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3319.v b/test-suite/bugs/closed/bug_3319.v
index 0b0aff29cb..9a9eac26c4 100644
--- a/test-suite/bugs/closed/bug_3319.v
+++ b/test-suite/bugs/closed/bug_3319.v
@@ -24,3 +24,4 @@ Section precategory.
   Proof.
     admit.
   Defined.
+End precategory.
diff --git a/test-suite/bugs/closed/bug_3320.v b/test-suite/bugs/closed/bug_3320.v
index a5c243d8e3..200c63b15c 100644
--- a/test-suite/bugs/closed/bug_3320.v
+++ b/test-suite/bugs/closed/bug_3320.v
@@ -3,3 +3,4 @@ Goal forall x : nat, True.
   assumption.
 Fail Qed.
 Undo.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3321.v b/test-suite/bugs/closed/bug_3321.v
index b6f10e533e..0718cd1257 100644
--- a/test-suite/bugs/closed/bug_3321.v
+++ b/test-suite/bugs/closed/bug_3321.v
@@ -17,3 +17,4 @@ intros.
 clear.
 try exists (path_universe admit). (* Toplevel input, characters 15-44:
 Anomaly: Uncaught exception Not_found(_). Please report. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3322.v b/test-suite/bugs/closed/bug_3322.v
index ab3025a6aa..eb391042dd 100644
--- a/test-suite/bugs/closed/bug_3322.v
+++ b/test-suite/bugs/closed/bug_3322.v
@@ -22,3 +22,5 @@ Section opposite.
   Transparent path_sigma_uncurried.
   (* This command should fail with "Error: Failed to progress.", as it does in 8.4; the simpl never directive should prevent simpl from progressing *)
   Fail progress simpl in *.
+  Abort.
+End opposite.
diff --git a/test-suite/bugs/closed/bug_3323.v b/test-suite/bugs/closed/bug_3323.v
index 4622634eaa..e81af07241 100644
--- a/test-suite/bugs/closed/bug_3323.v
+++ b/test-suite/bugs/closed/bug_3323.v
@@ -76,3 +76,4 @@ Error: In pattern-matching on term "x" the branch for constructor
   p2f (f2p (existT (fun I : Type => I -> A) x H)) =
   existT (fun I : Type => I -> A) x H".
  *)
+End AssumeFunext.
diff --git a/test-suite/bugs/closed/bug_3326.v b/test-suite/bugs/closed/bug_3326.v
index f0d8cbf704..1c12685353 100644
--- a/test-suite/bugs/closed/bug_3326.v
+++ b/test-suite/bugs/closed/bug_3326.v
@@ -17,3 +17,4 @@ Proof.
   clear.
   Fail apply aLeqRefl.
 Abort.
+End XXX.
diff --git a/test-suite/bugs/closed/bug_3331.v b/test-suite/bugs/closed/bug_3331.v
index 8594e45504..8047fc386b 100644
--- a/test-suite/bugs/closed/bug_3331.v
+++ b/test-suite/bugs/closed/bug_3331.v
@@ -29,3 +29,4 @@ Section groupoid_category.
     Set Typeclasses Debug.
     pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))).
 Abort.
+End groupoid_category.
diff --git a/test-suite/bugs/closed/bug_3337.v b/test-suite/bugs/closed/bug_3337.v
index cd7891f112..f8cfe985a9 100644
--- a/test-suite/bugs/closed/bug_3337.v
+++ b/test-suite/bugs/closed/bug_3337.v
@@ -2,3 +2,4 @@ Require Import Setoid.
 Goal forall x y : Set, x = y -> x = y.
 intros x y H.
 rewrite_strat subterms H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3338.v b/test-suite/bugs/closed/bug_3338.v
index 076cd5e6ea..57160503d4 100644
--- a/test-suite/bugs/closed/bug_3338.v
+++ b/test-suite/bugs/closed/bug_3338.v
@@ -2,3 +2,4 @@ Require Import Setoid.
 Goal forall x y : Set, x = y -> y = y.
 intros x y H.
 rewrite_strat try topdown terms H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3372.v b/test-suite/bugs/closed/bug_3372.v
index 91e3df76dd..eb70149a02 100644
--- a/test-suite/bugs/closed/bug_3372.v
+++ b/test-suite/bugs/closed/bug_3372.v
@@ -5,3 +5,4 @@ Fail exact hProp@{Set}. (* test that it fails, but is not an anomaly *)
 try (exact hProp@{Set}; fail 1). (* Toplevel input, characters 15-32:
 Anomaly: Uncaught exception Invalid_argument("Array.iter2", _).
 Please report. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3383.v b/test-suite/bugs/closed/bug_3383.v
index 25257644a6..b09b898adb 100644
--- a/test-suite/bugs/closed/bug_3383.v
+++ b/test-suite/bugs/closed/bug_3383.v
@@ -4,3 +4,4 @@ lazymatch goal with
 | [ |- context[match ?b as b' in bool return @?P b' with true => ?t | false => ?f end] ]
   => change (match b as b' in bool return P b' with true => t | false => f end) with (@bool_rect P t f b)
 end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3386.v b/test-suite/bugs/closed/bug_3386.v
index b8bb8bce09..74a7d1796c 100644
--- a/test-suite/bugs/closed/bug_3386.v
+++ b/test-suite/bugs/closed/bug_3386.v
@@ -15,3 +15,4 @@ Proof.
   try change Type@{i} with (Obj set_cat@{i}). (* check that it's not an anomaly *)
 (* Anomaly: Uncaught exception Invalid_argument("Array.iter2", _).
 Please report. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3390.v b/test-suite/bugs/closed/bug_3390.v
index eb3c4f4b9c..f4e405de72 100644
--- a/test-suite/bugs/closed/bug_3390.v
+++ b/test-suite/bugs/closed/bug_3390.v
@@ -7,3 +7,4 @@ Tactic Notation "basicapply" tactic0(tacfin) := idtac.
 
 Goal True.
 basicapply subst.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3393.v b/test-suite/bugs/closed/bug_3393.v
index ae8e41e29e..d2eb61e3e2 100644
--- a/test-suite/bugs/closed/bug_3393.v
+++ b/test-suite/bugs/closed/bug_3393.v
@@ -151,3 +151,5 @@ Unable to unify
   morphism := NaturalTransformation (D:=F z);
   compose := composet (D:=F z);
   associativity := associativityt (D:=F z) |}". *)
+  Abort.
+End lemmas.
diff --git a/test-suite/bugs/closed/bug_3427.v b/test-suite/bugs/closed/bug_3427.v
index 9a57ca7703..317efb0b32 100644
--- a/test-suite/bugs/closed/bug_3427.v
+++ b/test-suite/bugs/closed/bug_3427.v
@@ -194,3 +194,5 @@ instead of
        (fun x0 : setT (* Top.405 *) X0 =>
         @paths (* Top.404 *) (setT (* Top.404 *) Y0) (f0 x0) (f0 x))) Unit".
  *)
+  Abort.
+End AssumingUA.
diff --git a/test-suite/bugs/closed/bug_3441.v b/test-suite/bugs/closed/bug_3441.v
index d48c059acb..52acb996f8 100644
--- a/test-suite/bugs/closed/bug_3441.v
+++ b/test-suite/bugs/closed/bug_3441.v
@@ -21,3 +21,4 @@ Timeout 1 Time let H := fresh "H" in
      let x := constr:(let n := 17 in do_n n = do_n n) in
      let y := (eval lazy in x) in
      assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3461.v b/test-suite/bugs/closed/bug_3461.v
index 1885568bd2..cad28a558c 100644
--- a/test-suite/bugs/closed/bug_3461.v
+++ b/test-suite/bugs/closed/bug_3461.v
@@ -3,3 +3,4 @@ Lemma foo (b : bool) :
 Proof.
 eexists.
 Fail eexact (eq_refl b).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3469.v b/test-suite/bugs/closed/bug_3469.v
index 6aa3b56f8b..b43e65ab83 100644
--- a/test-suite/bugs/closed/bug_3469.v
+++ b/test-suite/bugs/closed/bug_3469.v
@@ -27,3 +27,4 @@ Proof.
 
 (* Toplevel input, characters 21-31:
 Error: Found no subterm matching "proj1_sig ?206" in the current *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3477.v b/test-suite/bugs/closed/bug_3477.v
index 3ed63604ea..0690c22670 100644
--- a/test-suite/bugs/closed/bug_3477.v
+++ b/test-suite/bugs/closed/bug_3477.v
@@ -7,3 +7,4 @@ Proof.
   evar (a : prod A B); evar (f : (prod A B -> Set)).
   let a' := (eval unfold a in a) in
   set(foo:=eq_refl : a' = (@pair _ _ (fst a') (snd a'))).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3480.v b/test-suite/bugs/closed/bug_3480.v
index 35e0c51a93..fd98232f96 100644
--- a/test-suite/bugs/closed/bug_3480.v
+++ b/test-suite/bugs/closed/bug_3480.v
@@ -46,3 +46,5 @@ x : xa <~=~> yb
 The term "morphism_isomorphic:@morphism (precategory_of_structures P) xa yb"
 has type "@morphism (precategory_of_structures P) xa yb"
 while it is expected to have type "morphism ?40 ?41 ?42". *)
+  Abort.
+End sip.
diff --git a/test-suite/bugs/closed/bug_3495.v b/test-suite/bugs/closed/bug_3495.v
index 102a2aba0d..7b0883f910 100644
--- a/test-suite/bugs/closed/bug_3495.v
+++ b/test-suite/bugs/closed/bug_3495.v
@@ -16,3 +16,4 @@ let e := match goal with |- R ?e _ => constr:(e) end in
 unify e (a (default_foo True)).
 subst b.
 reflexivity.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3513.v b/test-suite/bugs/closed/bug_3513.v
index f17fb2d9d0..462a615d91 100644
--- a/test-suite/bugs/closed/bug_3513.v
+++ b/test-suite/bugs/closed/bug_3513.v
@@ -71,3 +71,4 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
   Focus 2.
   (* As in 8.5, allow a shelved subgoal to remain *)
   apply reflexivity.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3539.v b/test-suite/bugs/closed/bug_3539.v
index b0c4b23702..3796a7b308 100644
--- a/test-suite/bugs/closed/bug_3539.v
+++ b/test-suite/bugs/closed/bug_3539.v
@@ -64,3 +64,4 @@ m : T3 (x' fst1 x2) (x' fst0 x2)
 Unable to unify "?25 (@pair ?23 ?24 (fst ?27) (snd ?27))" with
 "?25 ?27".
  *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3542.v b/test-suite/bugs/closed/bug_3542.v
index b6837a0c33..e9a8460622 100644
--- a/test-suite/bugs/closed/bug_3542.v
+++ b/test-suite/bugs/closed/bug_3542.v
@@ -4,3 +4,5 @@ Section foo.
   Goal True.
     pose (r := fun k => existT (fun g => forall x, f x = g x)
                                (fun x => projT1 (k x)) (fun x => projT2 (k x))).
+  Abort.
+End foo.
diff --git a/test-suite/bugs/closed/bug_3546.v b/test-suite/bugs/closed/bug_3546.v
index 55d718bd03..88724a52fc 100644
--- a/test-suite/bugs/closed/bug_3546.v
+++ b/test-suite/bugs/closed/bug_3546.v
@@ -15,3 +15,4 @@ z : Set
 w : Set
 Unable to unify "?31 ?191 = ?32 ?192" with "(x, y) = (z, w)".
  *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3554.v b/test-suite/bugs/closed/bug_3554.v
index 13a79cc840..2c88b79bc8 100644
--- a/test-suite/bugs/closed/bug_3554.v
+++ b/test-suite/bugs/closed/bug_3554.v
@@ -1 +1,2 @@
 Example foo (f : forall {_ : Type}, Type) : Type.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3561.v b/test-suite/bugs/closed/bug_3561.v
index 06ffef6829..7485c697f2 100644
--- a/test-suite/bugs/closed/bug_3561.v
+++ b/test-suite/bugs/closed/bug_3561.v
@@ -22,3 +22,4 @@ Goal forall (H0 H2 : Type) x p,
   match goal with
     | [ |- context[x (?f _)] ] => set(foo':=f)
   end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3562.v b/test-suite/bugs/closed/bug_3562.v
index 1a1410a3b1..bdb3fcb65f 100644
--- a/test-suite/bugs/closed/bug_3562.v
+++ b/test-suite/bugs/closed/bug_3562.v
@@ -4,3 +4,4 @@
 
 Theorem t: True.
 Fail destruct 0 as x.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3563.v b/test-suite/bugs/closed/bug_3563.v
index 961563ed4a..f6a84933b7 100644
--- a/test-suite/bugs/closed/bug_3563.v
+++ b/test-suite/bugs/closed/bug_3563.v
@@ -36,3 +36,4 @@ Goal forall (H H0 H1 : Type) (H2 : H1) (H3 : H1 -> (H1 -> H) * H0)
 (* Anomaly: Uncaught exception Not_found(_). Please report. *)
 
 (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3566.v b/test-suite/bugs/closed/bug_3566.v
index 84743e48f6..1255f0640f 100644
--- a/test-suite/bugs/closed/bug_3566.v
+++ b/test-suite/bugs/closed/bug_3566.v
@@ -21,3 +21,4 @@ Goal forall x y : Type, x = y.
   intros.
   pose proof ((fun H0 : idmap _ => (@path_universe _ _ (@lift x) (H0 x) @
                                                    (@path_universe _ _ (@lift x) (H0 x))^)))%path as H''.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3567.v b/test-suite/bugs/closed/bug_3567.v
index 00c9c05469..be05bb9453 100644
--- a/test-suite/bugs/closed/bug_3567.v
+++ b/test-suite/bugs/closed/bug_3567.v
@@ -66,3 +66,4 @@ which is ill-typed.
 Reason is: Pattern-matching expression on an object of inductive type prod
 has invalid information.
  *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3612.v b/test-suite/bugs/closed/bug_3612.v
index 33e5d532ad..b6dcd55346 100644
--- a/test-suite/bugs/closed/bug_3612.v
+++ b/test-suite/bugs/closed/bug_3612.v
@@ -52,3 +52,4 @@ Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
   pose (path_path_sigma B x x xx) as x''.
   clear x''.
   Check (path_path_sigma B x x xx).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3616.v b/test-suite/bugs/closed/bug_3616.v
index 688700260c..bb501f158c 100644
--- a/test-suite/bugs/closed/bug_3616.v
+++ b/test-suite/bugs/closed/bug_3616.v
@@ -1,3 +1,4 @@
 (* Was failing from April 2014 to September 2014 because of injection *)
 Goal forall P e es t, (e :: es = existT P tt t :: es)%list -> True.
 inversion 1.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3638.v b/test-suite/bugs/closed/bug_3638.v
index 4f1fcfecd3..4545738837 100644
--- a/test-suite/bugs/closed/bug_3638.v
+++ b/test-suite/bugs/closed/bug_3638.v
@@ -23,3 +23,4 @@ Goal forall (A B : Type) (x : O A * O B) (x0 : B),
 
 (* Toplevel input, characters 15-114:
 Anomaly: Bad recursive type. Please report. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3640.v b/test-suite/bugs/closed/bug_3640.v
index 5dff98ba23..d0d634bea5 100644
--- a/test-suite/bugs/closed/bug_3640.v
+++ b/test-suite/bugs/closed/bug_3640.v
@@ -29,3 +29,4 @@ Proof.
   Fail match type of H with
     | _ = negb ?T => unify T (f.1 true); fail 1 "still has f.1 true"
   end. (* Error: Tactic failure: still has f.1 true. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3641.v b/test-suite/bugs/closed/bug_3641.v
index 730ab3f431..eefec04851 100644
--- a/test-suite/bugs/closed/bug_3641.v
+++ b/test-suite/bugs/closed/bug_3641.v
@@ -19,3 +19,4 @@ Goal forall (A B : Type) (x : O A * O B) (x0 : B),
     | [ |- context[?e] ] => is_evar e; let e' := fresh "e'" in pose (e' := e)
   end.
   Fail change ?g with e'. (* Stack overflow *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3647.v b/test-suite/bugs/closed/bug_3647.v
index e91c004c77..80dd99709a 100644
--- a/test-suite/bugs/closed/bug_3647.v
+++ b/test-suite/bugs/closed/bug_3647.v
@@ -652,3 +652,4 @@ Goal    forall (ptest : program) (cond : Condition) (value : bool)
   subst_body; simpl.
   Fail refine (all_behead (projT2 _)).
   Unset Solve Unification Constraints. refine (all_behead (projT2 _)).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3648.v b/test-suite/bugs/closed/bug_3648.v
index 58aa161403..ec13115102 100644
--- a/test-suite/bugs/closed/bug_3648.v
+++ b/test-suite/bugs/closed/bug_3648.v
@@ -81,3 +81,4 @@ Found no subterm matching "F _1 (identity (fst x))" in the current goal. *)
   rewrite identity_of. (* Toplevel input, characters 15-34:
 Error:
 Found no subterm matching "morphism_of ?202 (identity ?203)" in the current goal. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3649.v b/test-suite/bugs/closed/bug_3649.v
index a664a1ef1d..2f907ccc32 100644
--- a/test-suite/bugs/closed/bug_3649.v
+++ b/test-suite/bugs/closed/bug_3649.v
@@ -58,3 +58,4 @@ Goal forall (C D : PreCategory) (G G' : Functor C D)
   let T0 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T0) end in
   let T1 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T1) end in
   progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3656.v b/test-suite/bugs/closed/bug_3656.v
index fb92e11630..cf32cac09d 100644
--- a/test-suite/bugs/closed/bug_3656.v
+++ b/test-suite/bugs/closed/bug_3656.v
@@ -51,3 +51,4 @@ Abort.
 
 Goal forall h, setT h = setT h.
 Proof. intro. progress unfold setT.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3657.v b/test-suite/bugs/closed/bug_3657.v
index 778fdab190..49c334e620 100644
--- a/test-suite/bugs/closed/bug_3657.v
+++ b/test-suite/bugs/closed/bug_3657.v
@@ -10,3 +10,4 @@ Defined.
 Goal @bar _ Set _ = (@bar _ (fun _ : Set => Set) _) nat.
 Proof.
   Fail change (bar (fun _ : Set => Set)) with (bar Set).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3660.v b/test-suite/bugs/closed/bug_3660.v
index be693886e6..f00ffef9e9 100644
--- a/test-suite/bugs/closed/bug_3660.v
+++ b/test-suite/bugs/closed/bug_3660.v
@@ -26,3 +26,4 @@ Goal forall (C D : hSet), IsEquiv (fun x : C = D => (equiv_path C D (ap setT x))
   apply @isequiv_compose; [ | admit ].
   Set Typeclasses Debug.
   typeclasses eauto.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3661.v b/test-suite/bugs/closed/bug_3661.v
index 1f13ffcf34..e040c9d39f 100644
--- a/test-suite/bugs/closed/bug_3661.v
+++ b/test-suite/bugs/closed/bug_3661.v
@@ -86,3 +86,4 @@ Goal forall (x3 x9 : PreCategory) (x12 f0 : Functor x9 x3)
         (@morphism_isomorphic (functor_category x9 x3) f0 x12 x35) _) x37)
 
 *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3667.v b/test-suite/bugs/closed/bug_3667.v
index 14a641f018..a0c112e7cc 100644
--- a/test-suite/bugs/closed/bug_3667.v
+++ b/test-suite/bugs/closed/bug_3667.v
@@ -21,3 +21,4 @@ Goal forall (A : PreCategory) (F : Functor A set_cat)
             (a : A) (x : F a) (nt :NaturalTransformation F F), x = x.
   intros.
   pose (fun c d m => ap10 (commutes nt c d m)).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3670.v b/test-suite/bugs/closed/bug_3670.v
index a4d5978b48..bdf4550a76 100644
--- a/test-suite/bugs/closed/bug_3670.v
+++ b/test-suite/bugs/closed/bug_3670.v
@@ -21,3 +21,4 @@ Module BAR_FROM_BAZ (baz : BAZ) <: BAR.
   Admitted.
 
 Fail End BAR_FROM_BAZ.
+Reset BAR_FROM_BAZ.
diff --git a/test-suite/bugs/closed/bug_3675.v b/test-suite/bugs/closed/bug_3675.v
index 93227ab852..529c1504cf 100644
--- a/test-suite/bugs/closed/bug_3675.v
+++ b/test-suite/bugs/closed/bug_3675.v
@@ -18,3 +18,4 @@ Proof.
                         (compose g f)
                         (compose f^-1 g^-1) _).
   exact (fun c => ap g (@eisretr _ _ f _ (g^-1 c)) @ (@eisretr _ _ g _ c)).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3685.v b/test-suite/bugs/closed/bug_3685.v
index 7a0c3e6f1d..5d91d84d98 100644
--- a/test-suite/bugs/closed/bug_3685.v
+++ b/test-suite/bugs/closed/bug_3685.v
@@ -73,3 +73,4 @@ Module Bad.
              object_of
              (fun CD C'D' FG => pointwise (fst FG) (snd FG))
              (fun _ _ => @Pidentity_of _ _ _ _).
+End Bad.
diff --git a/test-suite/bugs/closed/bug_3698.v b/test-suite/bugs/closed/bug_3698.v
index 3882eee97c..21978b7108 100644
--- a/test-suite/bugs/closed/bug_3698.v
+++ b/test-suite/bugs/closed/bug_3698.v
@@ -24,3 +24,4 @@ Proof.
                   g = g -> IsEquiv g) by admit.
   Eval compute in (@projT1 Type IsHSet (@equiv_inv _ _ _ (equiv_isequiv _ _ issig_hSet) X)).
   Fail apply H''. (* stack overflow *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3709.v b/test-suite/bugs/closed/bug_3709.v
index 815f5b9507..680a81da9e 100644
--- a/test-suite/bugs/closed/bug_3709.v
+++ b/test-suite/bugs/closed/bug_3709.v
@@ -22,3 +22,5 @@ Module Prim.
     intros h k f H.
     etransitivity.
     apply H.
+  Abort.
+End Prim.
diff --git a/test-suite/bugs/closed/bug_3710.v b/test-suite/bugs/closed/bug_3710.v
index b9e2798d88..07208ffa87 100644
--- a/test-suite/bugs/closed/bug_3710.v
+++ b/test-suite/bugs/closed/bug_3710.v
@@ -46,3 +46,4 @@ Local Notation cat := (@sub_pre_cat P).
 Goal forall (s d d' : cat) (m1 : morphism cat d d') (m2 : morphism cat s d),
        NaturalIsomorphism (m1 o m2) (m1 o m2)%functor.
 Fail exact (fun _ _ _ _ _ => reflexivity _).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3755.v b/test-suite/bugs/closed/bug_3755.v
index f0b542d31e..5485a0f8cf 100644
--- a/test-suite/bugs/closed/bug_3755.v
+++ b/test-suite/bugs/closed/bug_3755.v
@@ -14,3 +14,4 @@ Section param.
     @STex _ (fun x => P (@existT _ _ v x)).
 
   Check @existT _ _ STex STex.
+End param.
diff --git a/test-suite/bugs/closed/bug_3777.v b/test-suite/bugs/closed/bug_3777.v
index e203528fcc..9ca36cdd9f 100644
--- a/test-suite/bugs/closed/bug_3777.v
+++ b/test-suite/bugs/closed/bug_3777.v
@@ -15,3 +15,4 @@ Module WithPoly.
   Definition foo (A : Type@{i}) (B : Type@{i}) := A -> B.
   Set Printing Universes.
   Fail Check ((@foo : Set -> _ -> _) : _ -> Type -> _).
+End WithPoly.
diff --git a/test-suite/bugs/closed/bug_3815.v b/test-suite/bugs/closed/bug_3815.v
index 5fb4839847..a89f9ac307 100644
--- a/test-suite/bugs/closed/bug_3815.v
+++ b/test-suite/bugs/closed/bug_3815.v
@@ -7,3 +7,4 @@ Theorem t {A B C D} (f : A -> A) (g : B -> C) (h : C -> D)
 : f ∘ f = f.
 Proof.
   rewrite_strat topdown (hints core).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3828.v b/test-suite/bugs/closed/bug_3828.v
index ae11c6c96c..3c01dfd734 100644
--- a/test-suite/bugs/closed/bug_3828.v
+++ b/test-suite/bugs/closed/bug_3828.v
@@ -1,2 +1,3 @@
 Goal 0 = 0.
 Fail pose ?Goal.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3849.v b/test-suite/bugs/closed/bug_3849.v
index a8dc3af9cf..bde75afa69 100644
--- a/test-suite/bugs/closed/bug_3849.v
+++ b/test-suite/bugs/closed/bug_3849.v
@@ -6,3 +6,4 @@ Goal True.
 do 5 pose proof 0 as ?n0.
 foo n1 n2.
 bar n3 n4.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3854.v b/test-suite/bugs/closed/bug_3854.v
index 7e915f202b..877e4ba48b 100644
--- a/test-suite/bugs/closed/bug_3854.v
+++ b/test-suite/bugs/closed/bug_3854.v
@@ -20,3 +20,4 @@ Proof.
   pose (fun x => BuildhProp (~ mem x x)).
   refine (mem_induction (fun x => BuildhProp (~ mem x x)) _); simpl in *.
   admit.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3895.v b/test-suite/bugs/closed/bug_3895.v
index 8659ca2cbd..53fd6b2da2 100644
--- a/test-suite/bugs/closed/bug_3895.v
+++ b/test-suite/bugs/closed/bug_3895.v
@@ -20,3 +20,4 @@ Proof.
   change g with ((snd o pr1) o e).
   apply (ap (fun g => snd o pr1 o g)).
 (* Used to raise a not Found due to a "typo" in solve_evar_evar *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3896.v b/test-suite/bugs/closed/bug_3896.v
index b433922a21..5ccc9c5d3a 100644
--- a/test-suite/bugs/closed/bug_3896.v
+++ b/test-suite/bugs/closed/bug_3896.v
@@ -2,3 +2,4 @@ Goal True.
 pose proof 0 as n.
 Fail apply pair in n.
 (* Used to be an anomaly for a while *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3920.v b/test-suite/bugs/closed/bug_3920.v
index a4adb23cc2..25a76242ba 100644
--- a/test-suite/bugs/closed/bug_3920.v
+++ b/test-suite/bugs/closed/bug_3920.v
@@ -5,3 +5,4 @@ Lemma foo (H : P 3) : False.
 eapply or_introl in H.
 erewrite <- P_or in H.
 (* Error: No such hypothesis: H *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_3922.v b/test-suite/bugs/closed/bug_3922.v
index d88e8c3325..6e982f8103 100644
--- a/test-suite/bugs/closed/bug_3922.v
+++ b/test-suite/bugs/closed/bug_3922.v
@@ -83,3 +83,4 @@ Proof.
   refine (let g' := Trunc_ind (fun _ => P) g : merely X -> P in _);
     [ assumption.. | ].
   pose (g'' := Trunc_ind (fun _ => P) g : merely X -> P).
+Abort.
diff --git a/test-suite/bugs/closed/bug_3938.v b/test-suite/bugs/closed/bug_3938.v
index 35db82bd4c..a27600957a 100644
--- a/test-suite/bugs/closed/bug_3938.v
+++ b/test-suite/bugs/closed/bug_3938.v
@@ -6,3 +6,4 @@ Goal forall a b (f : nat -> Set) (R : nat -> nat -> Prop),
        Equivalence R -> R a b -> f a = f b.
   intros a b f H.
   intros. Fail rewrite H1.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3943.v b/test-suite/bugs/closed/bug_3943.v
index ac9c50369b..151a6ea275 100644
--- a/test-suite/bugs/closed/bug_3943.v
+++ b/test-suite/bugs/closed/bug_3943.v
@@ -48,3 +48,4 @@ Admitted.
 
 Definition ap_morphism_inverse_path_isomorphic (i j : Isomorphic s d) p q
 : ap (fun e : Isomorphic s d => e^-1)%morphism (path_isomorphic i j p) = q.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3944.v b/test-suite/bugs/closed/bug_3944.v
index 58e60f4f2e..c9e9795d9e 100644
--- a/test-suite/bugs/closed/bug_3944.v
+++ b/test-suite/bugs/closed/bug_3944.v
@@ -3,3 +3,4 @@ Definition C (T : Type) := T.
 Goal forall T (i : C T) (v : T), True.
 Proof.
 Fail setoid_rewrite plus_n_Sm.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3953.v b/test-suite/bugs/closed/bug_3953.v
index 167cecea8e..f473f63545 100644
--- a/test-suite/bugs/closed/bug_3953.v
+++ b/test-suite/bugs/closed/bug_3953.v
@@ -3,3 +3,4 @@ Goal forall (a b : unit), a = b -> exists c, b = c.
   intros.
   eexists.
   subst.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3974.v b/test-suite/bugs/closed/bug_3974.v
index 3d9e06b612..b166e73fa1 100644
--- a/test-suite/bugs/closed/bug_3974.v
+++ b/test-suite/bugs/closed/bug_3974.v
@@ -5,3 +5,4 @@ Module Type M (X : S).
   Fail Module P (X : S).
   (* Used to say: Anomaly: X already exists. Please report. *)
   (* Should rather say now: Error: X already exists. *)
+End M.
diff --git a/test-suite/bugs/closed/bug_3975.v b/test-suite/bugs/closed/bug_3975.v
index c7616b3ab6..afd35815df 100644
--- a/test-suite/bugs/closed/bug_3975.v
+++ b/test-suite/bugs/closed/bug_3975.v
@@ -6,3 +6,4 @@ Module Type P (X : S).
   Print M.
   (* Used to say: Anomaly: X already exists. Please report. *)
   (* Should rather : print something :-) *)
+End P.
diff --git a/test-suite/bugs/closed/bug_3993.v b/test-suite/bugs/closed/bug_3993.v
index 086d8dd0f3..a1ab3bf615 100644
--- a/test-suite/bugs/closed/bug_3993.v
+++ b/test-suite/bugs/closed/bug_3993.v
@@ -1,3 +1,4 @@
 (* Test smooth failure on not fully applied term to destruct with eqn: given *)
 Goal True.
 Fail induction S eqn:H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4018.v b/test-suite/bugs/closed/bug_4018.v
index 8895e09e02..d7929372ad 100644
--- a/test-suite/bugs/closed/bug_4018.v
+++ b/test-suite/bugs/closed/bug_4018.v
@@ -1,3 +1,4 @@
 (* Catching PatternMatchingFailure was lost at some point *)
 Goal nat -> True.
 Fail intros [=].
+Abort.
diff --git a/test-suite/bugs/closed/bug_4034.v b/test-suite/bugs/closed/bug_4034.v
index 3f7be4d1c7..5f1b60fc8d 100644
--- a/test-suite/bugs/closed/bug_4034.v
+++ b/test-suite/bugs/closed/bug_4034.v
@@ -23,3 +23,4 @@ Goal Foo.
   myexact !.
 Defined.
 *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_4035.v b/test-suite/bugs/closed/bug_4035.v
index ec246d097b..461a95e82d 100644
--- a/test-suite/bugs/closed/bug_4035.v
+++ b/test-suite/bugs/closed/bug_4035.v
@@ -11,3 +11,4 @@ Goal nat -> Type.
   lazymatch goal with
   | [ x : nat |- _ ] => dependent destruction x
   end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4057.v b/test-suite/bugs/closed/bug_4057.v
index 5b2e56f261..f5889d253c 100644
--- a/test-suite/bugs/closed/bug_4057.v
+++ b/test-suite/bugs/closed/bug_4057.v
@@ -208,3 +208,4 @@ P (parse_of_item_name__of__minimal_parse_of_name p') }.
     simpl in *.
     admit.
   Qed.
+End recursive_descent_parser.
diff --git a/test-suite/bugs/closed/bug_4089.v b/test-suite/bugs/closed/bug_4089.v
index fc1c504f14..38fbec0464 100644
--- a/test-suite/bugs/closed/bug_4089.v
+++ b/test-suite/bugs/closed/bug_4089.v
@@ -373,3 +373,4 @@ cannot be applied to the term
 This term has type "Type@{Top.892}" which should be coercible to
  "Type@{Top.882}".
 *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_4095.v b/test-suite/bugs/closed/bug_4095.v
index bc9380f90d..3d3015c383 100644
--- a/test-suite/bugs/closed/bug_4095.v
+++ b/test-suite/bugs/closed/bug_4095.v
@@ -85,3 +85,4 @@ tr : T -> T
 O2 : PointedOPred
 x0 : T
 H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_4101.v b/test-suite/bugs/closed/bug_4101.v
index b7c3e372aa..19e6f65805 100644
--- a/test-suite/bugs/closed/bug_4101.v
+++ b/test-suite/bugs/closed/bug_4101.v
@@ -17,3 +17,4 @@ Proof.
   intros.
   Set Debug Tactic Unification.
   apply path_forall.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4103.v b/test-suite/bugs/closed/bug_4103.v
index 92cc0279ac..690511a86c 100644
--- a/test-suite/bugs/closed/bug_4103.v
+++ b/test-suite/bugs/closed/bug_4103.v
@@ -10,3 +10,4 @@ Proof.
   (* Set Debug Tactic Unification. *)
   (* Set Debug RAKAM. *)
   reflexivity.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4116.v b/test-suite/bugs/closed/bug_4116.v
index 5932c9c56e..17c7bbe5eb 100644
--- a/test-suite/bugs/closed/bug_4116.v
+++ b/test-suite/bugs/closed/bug_4116.v
@@ -381,3 +381,5 @@ Section Grothendieck2.
       destruct x.
       simpl.
       erewrite @isotoid_1.
+  Abort.
+End Grothendieck2.
diff --git a/test-suite/bugs/closed/bug_4151.v b/test-suite/bugs/closed/bug_4151.v
index fc0b58cfe1..9ec8c01ac6 100644
--- a/test-suite/bugs/closed/bug_4151.v
+++ b/test-suite/bugs/closed/bug_4151.v
@@ -401,3 +401,5 @@ Section sound.
     assumption.
     Undo.
     eassumption. (* no applicable tactic *)
+  Abort.
+End sound.
diff --git a/test-suite/bugs/closed/bug_4165.v b/test-suite/bugs/closed/bug_4165.v
index 8e0a62d35c..5333a0f6cf 100644
--- a/test-suite/bugs/closed/bug_4165.v
+++ b/test-suite/bugs/closed/bug_4165.v
@@ -5,3 +5,4 @@ match eval cbv delta [s] in s with
 | context C[true] =>
   let C':=context C[false] in pose C' as s'
 end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4187.v b/test-suite/bugs/closed/bug_4187.v
index b13ca36a37..d729d1a287 100644
--- a/test-suite/bugs/closed/bug_4187.v
+++ b/test-suite/bugs/closed/bug_4187.v
@@ -244,6 +244,8 @@ Arguments productions _ : clear implicits.
 Arguments grammar _ : clear implicits.
 
 End ContextFreeGrammar.
+End Parsers.
+End ADTSynthesis.
 
 Module Export BaseTypes.
 
@@ -707,3 +709,6 @@ Section implementation.
          G'.
     intros str G'.
     Timeout 1 assert (pf' : G' -> Prop) by abstract admit.
+  Abort.
+End implementation.
+End BooleanRecognizer.
diff --git a/test-suite/bugs/closed/bug_4190.v b/test-suite/bugs/closed/bug_4190.v
index 2843488ba0..7e975587f6 100644
--- a/test-suite/bugs/closed/bug_4190.v
+++ b/test-suite/bugs/closed/bug_4190.v
@@ -13,3 +13,6 @@ Module Type F (Import M : C).
 Lemma foo : True.
 Proof.
 bar.
+Abort.
+
+End F.
diff --git a/test-suite/bugs/closed/bug_4205.v b/test-suite/bugs/closed/bug_4205.v
index c40dfcc1f3..b6cf214cf9 100644
--- a/test-suite/bugs/closed/bug_4205.v
+++ b/test-suite/bugs/closed/bug_4205.v
@@ -6,3 +6,4 @@ Inductive test : nat -> nat -> nat -> nat -> Prop :=
 
 Goal test 1 2 3 4.
 erewrite f_equal2 with (f := fun k l => test _ _ k l).
+Abort.
diff --git a/test-suite/bugs/closed/bug_4216.v b/test-suite/bugs/closed/bug_4216.v
index 60b1311ace..5b4f3da160 100644
--- a/test-suite/bugs/closed/bug_4216.v
+++ b/test-suite/bugs/closed/bug_4216.v
@@ -17,3 +17,4 @@ Let T_pure_id `{TMonad T} {A: Type} (t: A -> A) (x: T A):
         path (T_fzip A A (T_pure (A -> A) t) x) x.
   unfold T_fzip, T_pure.
   Fail rewrite (ret_unit_left (fun g a => ret (g a)) (fun x => x)).
+Abort.
diff --git a/test-suite/bugs/closed/bug_4217.v b/test-suite/bugs/closed/bug_4217.v
index 19973f30a7..af1fe2c755 100644
--- a/test-suite/bugs/closed/bug_4217.v
+++ b/test-suite/bugs/closed/bug_4217.v
@@ -4,3 +4,4 @@ Fixpoint ith_default
          {default_A : nat}
          {As : list nat}
          {struct As} : Set.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4221.v b/test-suite/bugs/closed/bug_4221.v
index bc120fb1ff..f433c85455 100644
--- a/test-suite/bugs/closed/bug_4221.v
+++ b/test-suite/bugs/closed/bug_4221.v
@@ -7,3 +7,4 @@ Goal (forall x : nat, x = 1 -> False) -> 1 = 1 -> False.
     | [ x : forall k : nat, _ |- _ ]
       => specialize (fun H0 => x 1 H0)
   end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4234.v b/test-suite/bugs/closed/bug_4234.v
index 348dd49d93..0da4313063 100644
--- a/test-suite/bugs/closed/bug_4234.v
+++ b/test-suite/bugs/closed/bug_4234.v
@@ -5,3 +5,4 @@ Definition dirprodpair {X Y : UU} := existT (fun x : X => Y).
 Definition funtoprodtoprod {X Y Z : UU} : { a : X -> Y & X -> Z }.
 Proof.
   refine (dirprodpair _ (fun x => _)).
+Abort.
diff --git a/test-suite/bugs/closed/bug_4240.v b/test-suite/bugs/closed/bug_4240.v
index 083c59fe68..0009844fb6 100644
--- a/test-suite/bugs/closed/bug_4240.v
+++ b/test-suite/bugs/closed/bug_4240.v
@@ -10,3 +10,4 @@ assert (H5 = new).
 unfold H5.
 unfold H1.
 exact (eq_refl new).
+Abort.
diff --git a/test-suite/bugs/closed/bug_4256.v b/test-suite/bugs/closed/bug_4256.v
index 3e5438cd46..a88bd28aa9 100644
--- a/test-suite/bugs/closed/bug_4256.v
+++ b/test-suite/bugs/closed/bug_4256.v
@@ -41,3 +41,4 @@ Proof.
   clear H x0.
   (** But this doesn't: *)
   pose (existT (fun x:X => Trunc -1 (x = point X)) (point X) (tr idpath)).
+Abort.
diff --git a/test-suite/bugs/closed/bug_4284.v b/test-suite/bugs/closed/bug_4284.v
index 0fff3026ff..167a562fe8 100644
--- a/test-suite/bugs/closed/bug_4284.v
+++ b/test-suite/bugs/closed/bug_4284.v
@@ -4,3 +4,4 @@ Theorem onefiber' {X : Type} (P : X -> Type) (x : X) : True.
 Proof.
 set (Q1 := total2 (fun f => pr1 P f = x)).
 set (f1:=fun q1 : Q1 => pr2 _ (pr1 _ q1)).
+Abort.
diff --git a/test-suite/bugs/closed/bug_4287.v b/test-suite/bugs/closed/bug_4287.v
index 757b71b2dd..de97431520 100644
--- a/test-suite/bugs/closed/bug_4287.v
+++ b/test-suite/bugs/closed/bug_4287.v
@@ -4,7 +4,7 @@ Universe b.
 
 Universe c.
 
-Definition U : Type@{b} := Type@{c}.
+Definition UU : Type@{b} := Type@{c}.
 
 Module Type MT.
 
@@ -17,6 +17,10 @@ Module M : MT.
 Print Universes.
 Fail End M.
 
+  Reset T.
+  Definition T := Prop.
+End M.
+
 Set Universe Polymorphism.
 
 (* This is a modified version of Hurkens with all universes floating *)
diff --git a/test-suite/bugs/closed/bug_4299.v b/test-suite/bugs/closed/bug_4299.v
index a1daa193ae..d4a2e19717 100644
--- a/test-suite/bugs/closed/bug_4299.v
+++ b/test-suite/bugs/closed/bug_4299.v
@@ -10,3 +10,4 @@ Module M : Foo with Definition U := Type : Type.
   Definition U := let X := Type in Type.
   Definition eq : Type = U := eq_refl.
 Fail End M.
+Reset M.
diff --git a/test-suite/bugs/closed/bug_4325.v b/test-suite/bugs/closed/bug_4325.v
index af69ca04b6..de3e4bfa8c 100644
--- a/test-suite/bugs/closed/bug_4325.v
+++ b/test-suite/bugs/closed/bug_4325.v
@@ -3,3 +3,4 @@ Proof.
   clear.
   intro H.
   erewrite (fun H' => H _ H').
+Abort.
diff --git a/test-suite/bugs/closed/bug_4347.v b/test-suite/bugs/closed/bug_4347.v
index 29686a26c1..3f68444040 100644
--- a/test-suite/bugs/closed/bug_4347.v
+++ b/test-suite/bugs/closed/bug_4347.v
@@ -15,3 +15,4 @@ Record Demonstration := mkDemo
 
 Theorem DemoError : Demonstration.
 Fail apply mkDemo. (*Anomaly: Uncaught exception Not_found. Please report.*)
+Abort.
diff --git a/test-suite/bugs/closed/bug_4378.v b/test-suite/bugs/closed/bug_4378.v
index 9d59165562..c50fd2c800 100644
--- a/test-suite/bugs/closed/bug_4378.v
+++ b/test-suite/bugs/closed/bug_4378.v
@@ -7,3 +7,4 @@ Tactic Notation "epose2" open_constr(a) tactic3(tac) :=
 Goal True.
   epose _. Undo.
   epose2 _ idtac.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4397.v b/test-suite/bugs/closed/bug_4397.v
index 3566353d84..576e8186dd 100644
--- a/test-suite/bugs/closed/bug_4397.v
+++ b/test-suite/bugs/closed/bug_4397.v
@@ -1,3 +1,4 @@
 Require Import Equality.
 Theorem foo (u : unit) (H : u = u) : True.
 dependent destruction H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4404.v b/test-suite/bugs/closed/bug_4404.v
index 38fed1936c..4125ea1c1b 100644
--- a/test-suite/bugs/closed/bug_4404.v
+++ b/test-suite/bugs/closed/bug_4404.v
@@ -1,3 +1,4 @@
 Inductive Foo : Type -> Type := foo A : Foo A.
 Goal True.
   remember Foo.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4412.v b/test-suite/bugs/closed/bug_4412.v
index 4b2aae0c7b..a1fb3de4db 100644
--- a/test-suite/bugs/closed/bug_4412.v
+++ b/test-suite/bugs/closed/bug_4412.v
@@ -2,3 +2,4 @@ Require Import Coq.Bool.Bool Coq.Setoids.Setoid.
 Goal forall (P : forall b : bool, b = true -> Type) (x y : bool) (H : andb x y = true) (H' : P _ H), True.
   intros.
   Fail rewrite Bool.andb_true_iff in H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4416.v b/test-suite/bugs/closed/bug_4416.v
index 62b90b4286..600a8aa311 100644
--- a/test-suite/bugs/closed/bug_4416.v
+++ b/test-suite/bugs/closed/bug_4416.v
@@ -2,3 +2,4 @@ Goal exists x, x.
 Unset Solve Unification Constraints.
 unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end.
 (* Error: Incorrect number of goals (expected 2 tactics). *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_4453.v b/test-suite/bugs/closed/bug_4453.v
index 009dd5e3ca..9248b2ab8c 100644
--- a/test-suite/bugs/closed/bug_4453.v
+++ b/test-suite/bugs/closed/bug_4453.v
@@ -6,3 +6,5 @@ Goal Type -> True.
 rename A into B.
 intros A.
 Fail apply foo.
+Abort.
+End Foo.
diff --git a/test-suite/bugs/closed/bug_4456.v b/test-suite/bugs/closed/bug_4456.v
index 56a7b4f6e9..7685552725 100644
--- a/test-suite/bugs/closed/bug_4456.v
+++ b/test-suite/bugs/closed/bug_4456.v
@@ -462,6 +462,9 @@ Section cfg.
 End cfg.
 
 End Valid.
+End ContextFreeGrammar.
+End Parsers.
+End Fiat.
 
 Section app.
   Context {Char : Type} {HSL : StringLike Char} (G : grammar Char)
@@ -645,3 +648,4 @@ Defined.
           abstract t_parse_production_for.
           abstract t_parse_production_for.
         Defined.
+End recursive_descent_parser.
diff --git a/test-suite/bugs/closed/bug_4462.v b/test-suite/bugs/closed/bug_4462.v
index c680518c6a..be6d2bea76 100644
--- a/test-suite/bugs/closed/bug_4462.v
+++ b/test-suite/bugs/closed/bug_4462.v
@@ -5,3 +5,4 @@ Require Setoid.
 
 Goal P -> Q.
 unshelve (rewrite pqrw).
+Abort.
diff --git a/test-suite/bugs/closed/bug_4464.v b/test-suite/bugs/closed/bug_4464.v
index f8e9405d93..a0c266c0ee 100644
--- a/test-suite/bugs/closed/bug_4464.v
+++ b/test-suite/bugs/closed/bug_4464.v
@@ -2,3 +2,4 @@ Goal True -> True.
 Proof.
   intro H'.
   let H := H' in destruct H; try destruct H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4471.v b/test-suite/bugs/closed/bug_4471.v
index 36efc42d47..dec181e430 100644
--- a/test-suite/bugs/closed/bug_4471.v
+++ b/test-suite/bugs/closed/bug_4471.v
@@ -4,3 +4,4 @@ Goal forall (A B : Type) (P : forall _ : prod A B, Type) (a : A) (b : B) (p p0 :
 Proof.
   intros.
   Fail generalize dependent (a, b).
+Abort.
diff --git a/test-suite/bugs/closed/bug_4479.v b/test-suite/bugs/closed/bug_4479.v
index 921579d1e1..442555b319 100644
--- a/test-suite/bugs/closed/bug_4479.v
+++ b/test-suite/bugs/closed/bug_4479.v
@@ -1,3 +1,4 @@
 Goal True.
 Fail autorewrite with foo.
 try autorewrite with foo.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4480.v b/test-suite/bugs/closed/bug_4480.v
index ec6ec7e5c2..da15e8cf33 100644
--- a/test-suite/bugs/closed/bug_4480.v
+++ b/test-suite/bugs/closed/bug_4480.v
@@ -9,3 +9,4 @@ Admitted.
 Goal True.
   Fail setoid_rewrite foo.
   Fail setoid_rewrite trueI.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4484.v b/test-suite/bugs/closed/bug_4484.v
index 6231e2d3df..adf7c82401 100644
--- a/test-suite/bugs/closed/bug_4484.v
+++ b/test-suite/bugs/closed/bug_4484.v
@@ -8,3 +8,4 @@ Check (match foo as k return foo = k -> True with
        | true => _
        | false => _
        end eq_refl).
+Abort.
diff --git a/test-suite/bugs/closed/bug_4511.v b/test-suite/bugs/closed/bug_4511.v
index 0027596e59..11ee4ccd6f 100644
--- a/test-suite/bugs/closed/bug_4511.v
+++ b/test-suite/bugs/closed/bug_4511.v
@@ -1,2 +1,3 @@
 Goal True.
 Fail evar I.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4527.v b/test-suite/bugs/closed/bug_4527.v
index 8749680e8d..4f8a8dd272 100644
--- a/test-suite/bugs/closed/bug_4527.v
+++ b/test-suite/bugs/closed/bug_4527.v
@@ -268,3 +268,5 @@ S)    : In@{Ou Oa i} O (x=y).
         rewrite O_indpaths_beta; reflexivity.
     Qed.
     Check inO_paths@{Type}.
+End Reflective_Subuniverse.
+End ReflectiveSubuniverses_Theory.
diff --git a/test-suite/bugs/closed/bug_4529.v b/test-suite/bugs/closed/bug_4529.v
index b16d81bd7c..8e04bdca86 100644
--- a/test-suite/bugs/closed/bug_4529.v
+++ b/test-suite/bugs/closed/bug_4529.v
@@ -42,3 +42,4 @@ End cofe_mixin.
     *
  intros x.
 apply equiv_dist.
+  Abort.
diff --git a/test-suite/bugs/closed/bug_4533.v b/test-suite/bugs/closed/bug_4533.v
index f9cccd5a56..d2f9fb9099 100644
--- a/test-suite/bugs/closed/bug_4533.v
+++ b/test-suite/bugs/closed/bug_4533.v
@@ -228,3 +228,5 @@ v = _) r,
     | [ |- ?G ] => fail 1 "bad" G
     end.
     Fail rewrite concat_p_pp.
+  Abort.
+End Lex_Reflective_Subuniverses.
diff --git a/test-suite/bugs/closed/bug_4574.v b/test-suite/bugs/closed/bug_4574.v
index f166eb84a9..cd6458c174 100644
--- a/test-suite/bugs/closed/bug_4574.v
+++ b/test-suite/bugs/closed/bug_4574.v
@@ -5,3 +5,4 @@ Definition block A (a : A) := a.
 Goal forall A (a : A), block Type nat.
 Proof.
 Fail reflexivity.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v
index 4ffd5f0f4b..a8a446cc9b 100644
--- a/test-suite/bugs/closed/bug_4580.v
+++ b/test-suite/bugs/closed/bug_4580.v
@@ -4,3 +4,4 @@ Class Foo (A : Type) := foo : A.
 
 Unset Refine Instance Mode.
 Program Instance f1 : Foo nat := S _.
+Next Obligation. exact 0. Defined.
diff --git a/test-suite/bugs/closed/bug_4596.v b/test-suite/bugs/closed/bug_4596.v
index 592fdb6580..bdd5edbdfb 100644
--- a/test-suite/bugs/closed/bug_4596.v
+++ b/test-suite/bugs/closed/bug_4596.v
@@ -12,3 +12,4 @@ Goal forall (S : Type) (b b0 : S -> nat -> bool) (str : S) (p : nat)
 Proof.
 intros ???????? H0.
 rewrite H0.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4644.v b/test-suite/bugs/closed/bug_4644.v
index f09b27c2b1..d8f284834c 100644
--- a/test-suite/bugs/closed/bug_4644.v
+++ b/test-suite/bugs/closed/bug_4644.v
@@ -50,3 +50,4 @@ Goal forall (T T' : Set) (a3 : list T), exists y2, forall (a4 : T' -> bool),
   (etransitivity; [ t | reflexivity ]) || fail 0 "too early".
   Undo.
   t.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4661.v b/test-suite/bugs/closed/bug_4661.v
index 03d2350a69..ffcfbdd7ea 100644
--- a/test-suite/bugs/closed/bug_4661.v
+++ b/test-suite/bugs/closed/bug_4661.v
@@ -8,3 +8,4 @@ End Func.
 
 Module Shortest_path (T : Test).
 Print Func.
+End Shortest_path.
diff --git a/test-suite/bugs/closed/bug_4673.v b/test-suite/bugs/closed/bug_4673.v
index 0d49c6d9be..f5ee4e3b57 100644
--- a/test-suite/bugs/closed/bug_4673.v
+++ b/test-suite/bugs/closed/bug_4673.v
@@ -55,3 +55,4 @@ Goal    forall (Char : Type) (P : forall _ : list bool, Prop) (l : list bool) (l
   setoid_rewrite H || fail 0 "too early".
   Undo.
   setoid_rewrite H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4725.v b/test-suite/bugs/closed/bug_4725.v
index fd5e0fb60d..3c014ea17c 100644
--- a/test-suite/bugs/closed/bug_4725.v
+++ b/test-suite/bugs/closed/bug_4725.v
@@ -30,9 +30,10 @@ Proof. intros. apply remove_le. Qed.
 
 (* Program version *)
 
-Program Fixpoint nubV `{eqDecV : @EqDec V eqV equivV} (l : list V)
+Program Fixpoint nubV' `{eqDecV : @EqDec V eqV equivV} (l : list V)
         {  measure (@length V l) lt } :=
     match l with
       | nil => nil
-      | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) _
+      | x::xs => x :: @nubV' V eqV equivV eqDecV (removeV x xs) _
     end.
+Next Obligation. apply remove_le. Defined.
diff --git a/test-suite/bugs/closed/bug_4811.v b/test-suite/bugs/closed/bug_4811.v
index fe6e65a0f0..b90257cb3f 100644
--- a/test-suite/bugs/closed/bug_4811.v
+++ b/test-suite/bugs/closed/bug_4811.v
@@ -1683,3 +1683,4 @@ Goal    forall x9 x8 x7 x6 x5 x4 x3 x2 x1 x0 y9 y8 y7 y6 y5 y4 y3 y2 y1 y0 : Z,
   (timeout 1 (apply f_equal; reflexivity)) || fail 0 "too early".
   Undo.
   Time Timeout 1 f_equal. (* Finished transaction in 0. secs (0.3u,0.s) in 8.4 *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_4813.v b/test-suite/bugs/closed/bug_4813.v
index 5f8ea74c1a..d1a2ebe820 100644
--- a/test-suite/bugs/closed/bug_4813.v
+++ b/test-suite/bugs/closed/bug_4813.v
@@ -7,3 +7,4 @@ Definition reflexivityValid (_ : unit) := True.
 Definition reflexivityProver_correct : ProverT_correct {| Facts := unit |}.
 Proof.
     eapply Build_ProverT_correct with (Valid := reflexivityValid).
+Abort.
diff --git a/test-suite/bugs/closed/bug_4818.v b/test-suite/bugs/closed/bug_4818.v
index 7dc6e65725..186c4425c1 100644
--- a/test-suite/bugs/closed/bug_4818.v
+++ b/test-suite/bugs/closed/bug_4818.v
@@ -22,3 +22,4 @@ Admitted.
 (*
 Anomaly: Universe Product.5189 undefined. Please report.
 *)
+End Product.
diff --git a/test-suite/bugs/closed/bug_4893.v b/test-suite/bugs/closed/bug_4893.v
index 9a35bcf954..1b1ca7c108 100644
--- a/test-suite/bugs/closed/bug_4893.v
+++ b/test-suite/bugs/closed/bug_4893.v
@@ -2,3 +2,4 @@ Goal True.
 evar (P: Prop).
 assert (H : P); [|subst P]; [exact I|].
 let T := type of H in not_evar T.
+Abort.
diff --git a/test-suite/bugs/closed/bug_4969.v b/test-suite/bugs/closed/bug_4969.v
index 4dee41e221..d6d3021200 100644
--- a/test-suite/bugs/closed/bug_4969.v
+++ b/test-suite/bugs/closed/bug_4969.v
@@ -9,3 +9,4 @@ Proof. auto. Qed.
 Goal True.
   class_apply @silly; [reflexivity|].
   reflexivity. Fail Qed.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5045.v b/test-suite/bugs/closed/bug_5045.v
index dc38738d8f..bda2adc760 100644
--- a/test-suite/bugs/closed/bug_5045.v
+++ b/test-suite/bugs/closed/bug_5045.v
@@ -1,3 +1,4 @@
 Axiom silly : 1 = 1 -> nat -> nat.
 Goal forall pf : 1 = 1, silly pf 0 = 0 -> True.
   Fail generalize (@eq nat).
+Abort.
diff --git a/test-suite/bugs/closed/bug_5078.v b/test-suite/bugs/closed/bug_5078.v
index ca73cbcc18..f07085d900 100644
--- a/test-suite/bugs/closed/bug_5078.v
+++ b/test-suite/bugs/closed/bug_5078.v
@@ -3,3 +3,4 @@ Tactic Notation "unfold_hyp" hyp(H) := cbv delta [H].
 Goal True -> Type.
   intro H''.
   Fail unfold_hyp H''.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5093.v b/test-suite/bugs/closed/bug_5093.v
index 3ded4dd304..4b6d774405 100644
--- a/test-suite/bugs/closed/bug_5093.v
+++ b/test-suite/bugs/closed/bug_5093.v
@@ -9,3 +9,4 @@ Goal P 100.
 Proof.
 Fail typeclasses eauto 100 with foobar.
 typeclasses eauto 101 with foobar.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5095.v b/test-suite/bugs/closed/bug_5095.v
index b6f38e3e84..b8d97f0eb2 100644
--- a/test-suite/bugs/closed/bug_5095.v
+++ b/test-suite/bugs/closed/bug_5095.v
@@ -3,3 +3,4 @@ Goal let x := Set in let y := x in True.
   intros x y.
   (* There used to have a too strict dependency test there *)
   set (s := Set) in (value of x).
+Abort.
diff --git a/test-suite/bugs/closed/bug_5153.v b/test-suite/bugs/closed/bug_5153.v
index be6407b5fa..80d308f782 100644
--- a/test-suite/bugs/closed/bug_5153.v
+++ b/test-suite/bugs/closed/bug_5153.v
@@ -6,3 +6,4 @@ Goal forall (H : forall t : some_type, @Ty t -> False) (H' : False -> 1 = 2), 1
 Proof.
 intros H H'.
 specialize (H' (@H _ O)). (* was failing *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_5180.v b/test-suite/bugs/closed/bug_5180.v
index 05603a048c..c26ce52da2 100644
--- a/test-suite/bugs/closed/bug_5180.v
+++ b/test-suite/bugs/closed/bug_5180.v
@@ -62,3 +62,4 @@ The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type
  *)
   all:compute in *.
   all:exact x.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5193.v b/test-suite/bugs/closed/bug_5193.v
index cc8739afe6..0a52dcdef1 100644
--- a/test-suite/bugs/closed/bug_5193.v
+++ b/test-suite/bugs/closed/bug_5193.v
@@ -12,3 +12,4 @@ Context `{Finx_eqdec : forall n, Eqdec (Finx n)}.
 Goal {x : Type & Eqdec x}.
   eexists.
   try typeclasses eauto 1 with typeclass_instances.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5203.v b/test-suite/bugs/closed/bug_5203.v
index b0161cc530..2c4d1a9fb7 100644
--- a/test-suite/bugs/closed/bug_5203.v
+++ b/test-suite/bugs/closed/bug_5203.v
@@ -2,3 +2,4 @@ Goal True.
   Typeclasses eauto := debug.
   Fail solve [ typeclasses eauto ].
   Fail typeclasses eauto.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5219.v b/test-suite/bugs/closed/bug_5219.v
index f7cec1a0cf..6798c1ae4d 100644
--- a/test-suite/bugs/closed/bug_5219.v
+++ b/test-suite/bugs/closed/bug_5219.v
@@ -8,3 +8,4 @@ Goal forall x : sigT (fun x => x = 1), True.
   lazymatch goal with
   | [ H : _ = _ |- _ ] => idtac
   end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5321.v b/test-suite/bugs/closed/bug_5321.v
index 3c32a4cb4d..37866fcc94 100644
--- a/test-suite/bugs/closed/bug_5321.v
+++ b/test-suite/bugs/closed/bug_5321.v
@@ -16,3 +16,4 @@ Proof.
   intros.
   etransitivity; [ | exact (proj2_sig_path H) ].
   Fail clearbody fpf.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5322.v b/test-suite/bugs/closed/bug_5322.v
index 01aec8f29b..7664d312e9 100644
--- a/test-suite/bugs/closed/bug_5322.v
+++ b/test-suite/bugs/closed/bug_5322.v
@@ -12,3 +12,4 @@ Definition bound_op {var}
   refine match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with
          | _ => _
          end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5359.v b/test-suite/bugs/closed/bug_5359.v
index a5a96db2c3..1f202e4396 100644
--- a/test-suite/bugs/closed/bug_5359.v
+++ b/test-suite/bugs/closed/bug_5359.v
@@ -216,3 +216,4 @@ Goal False.
                                 (Ring_polynom.PEX Z 3)))) :: nil)%list ) in
     Nsatz.nsatz_compute
           (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))).
+Abort.
diff --git a/test-suite/bugs/closed/bug_5372.v b/test-suite/bugs/closed/bug_5372.v
index e60244cd1d..e36b7a5d70 100644
--- a/test-suite/bugs/closed/bug_5372.v
+++ b/test-suite/bugs/closed/bug_5372.v
@@ -6,3 +6,4 @@ Function odd (n:nat) :=
   | S n => true
   end
 with even (n:nat) := false.
+Reset odd.
diff --git a/test-suite/bugs/closed/bug_5414.v b/test-suite/bugs/closed/bug_5414.v
index 2522a274fb..bf4e7133b7 100644
--- a/test-suite/bugs/closed/bug_5414.v
+++ b/test-suite/bugs/closed/bug_5414.v
@@ -10,3 +10,4 @@ Goal foo.
 intros k. elim k. (* elim because elim keeps names *)
 intros.
 Check a. (* We check that the name is "a" *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_5434.v b/test-suite/bugs/closed/bug_5434.v
index 5d2460face..b15e947531 100644
--- a/test-suite/bugs/closed/bug_5434.v
+++ b/test-suite/bugs/closed/bug_5434.v
@@ -16,3 +16,4 @@ Goal True.
   | sig (fun a : ?A => ?P) -> _
     => pose (fun a : A => a = a /\ P = P)
   end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5449.v b/test-suite/bugs/closed/bug_5449.v
index d7fc2aaa00..47ecba956e 100644
--- a/test-suite/bugs/closed/bug_5449.v
+++ b/test-suite/bugs/closed/bug_5449.v
@@ -4,3 +4,4 @@ Require Import Coq.PArith.BinPos.
 Goal forall x y, {Pos.compare_cont Gt x y = Gt} + {Pos.compare_cont Gt x y <> Gt}.
 intros.
 decide equality.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5476.v b/test-suite/bugs/closed/bug_5476.v
index 7c0c2c1dfd..4bfa011762 100644
--- a/test-suite/bugs/closed/bug_5476.v
+++ b/test-suite/bugs/closed/bug_5476.v
@@ -26,3 +26,4 @@ Proof.
                  end
                | fail 1 "could not find" X ]
     end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5486.v b/test-suite/bugs/closed/bug_5486.v
index b1ddfe24bf..b086fbfa6e 100644
--- a/test-suite/bugs/closed/bug_5486.v
+++ b/test-suite/bugs/closed/bug_5486.v
@@ -13,3 +13,4 @@ Goal forall (T : Type) (p : prod (prod T T) bool) (Fm : Set) (f : Fm) (k :
   | [ |- ?f (let (a, b) := ?d in @?e a b) = ?rhs ]
     => pose (let (a, b) := d in e a b) as t0
   end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5487.v b/test-suite/bugs/closed/bug_5487.v
index 9b995f4503..36999f76df 100644
--- a/test-suite/bugs/closed/bug_5487.v
+++ b/test-suite/bugs/closed/bug_5487.v
@@ -7,3 +7,4 @@ Proof.
   | [ |- ?x = ?y ]
     => match x with y => idtac end
   end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5501.v b/test-suite/bugs/closed/bug_5501.v
index 24739a3658..e5e8a89278 100644
--- a/test-suite/bugs/closed/bug_5501.v
+++ b/test-suite/bugs/closed/bug_5501.v
@@ -19,3 +19,4 @@ Global Instance Pred_All_instance (A : Pred_All) : All A := P'_All A.
 Definition Pred_All_proof {A : Pred_All} (a : A) : P A a.
 Proof.
 solve[auto using proof].
+Abort.
diff --git a/test-suite/bugs/closed/bug_5547.v b/test-suite/bugs/closed/bug_5547.v
index 79633f4893..ee4a9b083a 100644
--- a/test-suite/bugs/closed/bug_5547.v
+++ b/test-suite/bugs/closed/bug_5547.v
@@ -14,3 +14,4 @@ Fail refine (fun x
              | (y,J) => true
              end
          ).
+Abort.
diff --git a/test-suite/bugs/closed/bug_5578.v b/test-suite/bugs/closed/bug_5578.v
index 19d36e635d..a8a4dd6e30 100644
--- a/test-suite/bugs/closed/bug_5578.v
+++ b/test-suite/bugs/closed/bug_5578.v
@@ -55,3 +55,4 @@ Goal forall (Rat : Set) (PositiveMap_t : Set -> Set)
                          (Bind (k eta) (fun rands =>
                           ret_bool (interp_term_fixed_t_x eta (adv' eta) rands  ?= interp_term_fixed_t_x eta (adv' eta) rands)))))).
  (* Error: Anomaly "Signature and its instance do not match." Please report at http://coq.inria.fr/bugs/. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_5666.v b/test-suite/bugs/closed/bug_5666.v
index d55a6e57b4..1fe7fa19eb 100644
--- a/test-suite/bugs/closed/bug_5666.v
+++ b/test-suite/bugs/closed/bug_5666.v
@@ -2,3 +2,4 @@ Inductive foo := Foo : False -> foo.
 Goal foo.
 try (constructor ; fail 0).
 Fail try (constructor ; fail 1).
+Abort.
diff --git a/test-suite/bugs/closed/bug_5671.v b/test-suite/bugs/closed/bug_5671.v
index c9a085045a..dfa7ed5d69 100644
--- a/test-suite/bugs/closed/bug_5671.v
+++ b/test-suite/bugs/closed/bug_5671.v
@@ -5,3 +5,4 @@ Axiom a : forall x, x=0 -> True.
 Lemma lem (x y1 y2:nat) (H:x=0) (H0:eq y1 y2) : y1 = y2.
 specialize a with (1:=H). clear H x. intros _.
 setoid_rewrite H0.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5707.v b/test-suite/bugs/closed/bug_5707.v
index 785844c66d..096069049a 100644
--- a/test-suite/bugs/closed/bug_5707.v
+++ b/test-suite/bugs/closed/bug_5707.v
@@ -10,3 +10,4 @@ Inductive foo := Foo { proj1 : nat; proj2 : nat }.
 
 Goal forall x : foo, True.
 Proof. intros x. destruct x.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5741.v b/test-suite/bugs/closed/bug_5741.v
index f6598f192d..27bf9e76ef 100644
--- a/test-suite/bugs/closed/bug_5741.v
+++ b/test-suite/bugs/closed/bug_5741.v
@@ -2,3 +2,4 @@
 
 Goal True.
 info_trivial.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5749.v b/test-suite/bugs/closed/bug_5749.v
index 81bfe351c5..7a2944dc7e 100644
--- a/test-suite/bugs/closed/bug_5749.v
+++ b/test-suite/bugs/closed/bug_5749.v
@@ -16,3 +16,6 @@ a))).
     SetUnfold (Q)
               (fold_right _ _ (fun (s : lType2) => let (P, _) := s in and (P
 m)) (Q) (fhl1)).
+  Abort.
+
+End Filter_Help.
diff --git a/test-suite/bugs/closed/bug_5750.v b/test-suite/bugs/closed/bug_5750.v
index 6d0e21f5d0..d5527d9303 100644
--- a/test-suite/bugs/closed/bug_5750.v
+++ b/test-suite/bugs/closed/bug_5750.v
@@ -1,3 +1,4 @@
 (* Check printability of the hole of the context *)
 Goal 0 = 0.
 match goal with |- context c [0] => idtac c end.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5757.v b/test-suite/bugs/closed/bug_5757.v
index 0d0f2eed44..4d90c44cfe 100644
--- a/test-suite/bugs/closed/bug_5757.v
+++ b/test-suite/bugs/closed/bug_5757.v
@@ -74,3 +74,4 @@ match goal with
     change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v)
 end.
 Abort.
+End Tests.
diff --git a/test-suite/bugs/closed/bug_6534.v b/test-suite/bugs/closed/bug_6534.v
index f5013994c5..8e3c2bb1a1 100644
--- a/test-suite/bugs/closed/bug_6534.v
+++ b/test-suite/bugs/closed/bug_6534.v
@@ -5,3 +5,4 @@ refine ((fun x x => _ tt) tt tt).
 let t := match goal with [ |- ?P ] => P end in
 let _ := type of t in
 idtac.
+Abort.
diff --git a/test-suite/bugs/closed/bug_6631.v b/test-suite/bugs/closed/bug_6631.v
index 100dc13fc8..0833ae17ff 100644
--- a/test-suite/bugs/closed/bug_6631.v
+++ b/test-suite/bugs/closed/bug_6631.v
@@ -5,3 +5,4 @@ Proof.
   transitivity 2; [refine (eq_refl 2)|].
   transitivity 2.
   2:abstract exact (eq_refl 2).
+Abort.
diff --git a/test-suite/bugs/closed/bug_7392.v b/test-suite/bugs/closed/bug_7392.v
index cf465c6588..df4408d899 100644
--- a/test-suite/bugs/closed/bug_7392.v
+++ b/test-suite/bugs/closed/bug_7392.v
@@ -7,3 +7,4 @@ eapply H0.
 clear H1.
 apply ER.
 simpl.
+Abort.
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.
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.
diff --git a/test-suite/modules/SeveralWith.v b/test-suite/modules/SeveralWith.v
index bbf72a7648..4426f2710a 100644
--- a/test-suite/modules/SeveralWith.v
+++ b/test-suite/modules/SeveralWith.v
@@ -10,3 +10,4 @@ End ES.
 Module Make
   (AX : S)
   (X : ES with Definition A := AX.A with Definition eq := @eq AX.A).
+End Make.
diff --git a/test-suite/modules/WithDefUBinders.v b/test-suite/modules/WithDefUBinders.v
index e683455162..00a93b5fdf 100644
--- a/test-suite/modules/WithDefUBinders.v
+++ b/test-suite/modules/WithDefUBinders.v
@@ -13,3 +13,5 @@ Fail Module M' : T with Definition foo := Type.
 (* Without the binder expression we have to do trickery to get the
    universes in the right order. *)
 Module M' : T with Definition foo := let t := Type in t.
+Definition foo := let t := Type in t.
+End M'.
diff --git a/test-suite/modules/errors.v b/test-suite/modules/errors.v
index d1658786ea..487de5801c 100644
--- a/test-suite/modules/errors.v
+++ b/test-suite/modules/errors.v
@@ -1,70 +1,90 @@
+(* coq-prog-args: ("-impredicative-set") *)
 (* Inductive mismatches *)
 
 Module Type SA. Inductive TA : nat -> Prop := CA : nat -> TA 0. End SA.
 Module MA : SA. Inductive TA : Prop := CA : bool -> TA. Fail End MA.
+Reset Initial.
 
-Module Type SA. Inductive TA := CA : nat -> TA. End SA.
-Module MA : SA. Inductive TA := CA : bool -> TA. Fail End MA.
+Module Type SA0. Inductive TA0 := CA0 : nat -> TA0. End SA0.
+Module MA0 : SA0. Inductive TA0 := CA0 : bool -> TA0. Fail End MA0.
+Reset Initial.
 
-Module Type SA. Inductive TA := CA : nat -> TA. End SA.
-Module MA : SA. Inductive TA := CA : bool -> nat -> TA. Fail End MA.
+Module Type SA1. Inductive TA1 := CA1 : nat -> TA1. End SA1.
+Module MA1 : SA1. Inductive TA1 := CA1 : bool -> nat -> TA1. Fail End MA1.
+Reset Initial.
 
 Module Type SA2. Inductive TA2 := CA2 : nat -> TA2. End SA2.
 Module MA2 : SA2. Inductive TA2 := CA2 : nat -> TA2 | DA2 : TA2. Fail End MA2.
+Reset Initial.
 
 Module Type SA3. Inductive TA3 := CA3 : nat -> TA3. End SA3.
 Module MA3 : SA3. Inductive TA3 := CA3 : nat -> TA3 with UA3 := DA3. Fail End MA3.
+Reset Initial.
 
 Module Type SA4. Inductive TA4 := CA4 : nat -> TA4 with UA4 := DA4. End SA4.
 Module MA4 : SA4. Inductive TA4 := CA4 : nat -> TA4 with VA4 := DA4. Fail End MA4.
+Reset Initial.
 
 Module Type SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := DA5. End SA5.
 Module MA5 : SA5. Inductive TA5 := CA5 : nat -> TA5 with UA5 := EA5. Fail End MA5.
+Reset Initial.
 
 Module Type SA6. Inductive TA6 (A:Type) := CA6 : A -> TA6 A. End SA6.
 Module MA6 : SA6. Inductive TA6 (A B:Type):= CA6 : A -> TA6 A B. Fail End MA6.
+Reset Initial.
 
 Module Type SA7. Inductive TA7 (A:Type) := CA7 : A -> TA7 A. End SA7.
 Module MA7 : SA7. CoInductive TA7 (A:Type):= CA7 : A -> TA7 A. Fail End MA7.
+Reset Initial.
 
 Module Type SA8. CoInductive TA8 (A:Type) := CA8 : A -> TA8 A. End SA8.
 Module MA8 : SA8. Inductive TA8 (A:Type):= CA8 : A -> TA8 A. Fail End MA8.
+Reset Initial.
 
 Module Type SA9. Record TA9 (A:Type) := { CA9 : A }. End SA9.
 Module MA9 : SA9. Inductive TA9 (A:Type):= CA9 : A -> TA9 A. Fail End MA9.
+Reset Initial.
 
 Module Type SA10. Inductive TA10 (A:Type) := CA10 : A -> TA10 A. End SA10.
 Module MA10 : SA10. Record TA10 (A:Type):= { CA10 : A }. Fail End MA10.
+Reset Initial.
 
 Module Type SA11. Record TA11 (A:Type):= { CA11 : A }. End SA11.
 Module MA11 : SA11. Record TA11 (A:Type):= { DA11 : A }. Fail End MA11.
+Reset Initial.
 
 (* Basic mismatches *)
 Module Type SB. Inductive TB := CB : nat -> TB. End SB.
 Module MB : SB. Module Type TB. End TB. Fail End MB.
+Inductive TB := CB : nat -> TB. End MB.
 
 Module Type SC. Module Type TC. End TC. End SC.
 Module MC : SC. Inductive TC := CC : nat -> TC. Fail End MC.
+Reset Initial.
 
 Module Type SD. Module TD. End TD. End SD.
 Module MD : SD. Inductive TD := DD : nat -> TD. Fail End MD.
+Reset Initial.
 
 Module Type SE. Definition DE := nat. End SE.
 Module ME : SE. Definition DE := bool. Fail End ME.
+Reset Initial.
 
 Module Type SF. Parameter DF : nat. End SF.
 Module MF : SF. Definition DF := bool. Fail End MF.
+Reset Initial.
 
 (* Needs a type constraint in module type *)
 Module Type SG. Definition DG := Type. End SG.
 Module MG : SG. Definition DG := Type : Type. Fail End MG.
+Reset Initial.
 
 (* Should work *)
-Module Type SA7. Inductive TA7 (A:Type) := CA7 : A -> TA7 A. End SA7.
-Module MA7 : SA7. Inductive TA7 (B:Type):= CA7 : B -> TA7 B. End MA7.
+Module Type SA70. Inductive TA70 (A:Type) := CA70 : A -> TA70 A. End SA70.
+Module MA70 : SA70. Inductive TA70 (B:Type):= CA70 : B -> TA70 B. End MA70.
 
-Module Type SA11. Record TA11 (B:Type):= { CA11 : B }. End SA11.
-Module MA11 : SA11. Record TA11 (A:Type):= { CA11 : A }. End MA11.
+Module Type SA12. Record TA12 (B:Type):= { CA12 : B }. End SA12.
+Module MA12 : SA12. Record TA12 (A:Type):= { CA12 : A }. End MA12.
 
-Module Type SE. Parameter DE : Type. End SE.
-Module ME : SE. Definition DE := Type : Type. End ME.
+Module Type SH. Parameter DH : Type. End SH.
+Module MH : SH. Definition DH := Type : Type. End MH.
diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v
index dce2ffd50b..fe1372298e 100644
--- a/test-suite/modules/fun_objects.v
+++ b/test-suite/modules/fun_objects.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-impredicative-set") *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index e4fa7044e7..43718a0f07 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -187,6 +187,7 @@ let p := fresh "p" in
   |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end)
   end.
 Show.
+Abort.
 
 Set Printing Allow Match Default Clause.
 
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index c9b5091347..7375227827 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -31,3 +31,6 @@ Abort.
 Fail Goal forall a f, f a = 0.
 Fail Goal forall f x, id f x = 0.
 Fail Goal forall f P,  P (f 0).
+
+Definition t := unit.
+End M.
diff --git a/test-suite/output/Existentials.v b/test-suite/output/Existentials.v
index 7388468399..924f1f5592 100644
--- a/test-suite/output/Existentials.v
+++ b/test-suite/output/Existentials.v
@@ -12,3 +12,5 @@ clearbody q.
 clear p. (* Error ... *)
 
 Show Existentials.
+Abort.
+End Test.
diff --git a/test-suite/output/Match_subterm.v b/test-suite/output/Match_subterm.v
index 2c44b1879f..bf862c946d 100644
--- a/test-suite/output/Match_subterm.v
+++ b/test-suite/output/Match_subterm.v
@@ -4,3 +4,4 @@ match goal with
   idtac v ; fail
 | _ => idtac 2
 end.
+Abort.
diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v
index 327643dc57..7f3b332d7d 100644
--- a/test-suite/output/Naming.v
+++ b/test-suite/output/Naming.v
@@ -89,3 +89,4 @@ Show.
 apply H with (a:=a). (* test compliance with printing *)
 Abort.
 
+End A.
diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v
index 02b7eada83..9cf6ad35b8 100644
--- a/test-suite/output/ShowMatch.v
+++ b/test-suite/output/ShowMatch.v
@@ -11,3 +11,4 @@ Module B.
   Inductive foo := f.
   (* local foo shadows A.foo, so constructor "f" needs disambiguation *)
   Show Match A.foo. 
+End B.
diff --git a/test-suite/output/ShowProof.v b/test-suite/output/ShowProof.v
index 73ecaf2200..19822ac50e 100644
--- a/test-suite/output/ShowProof.v
+++ b/test-suite/output/ShowProof.v
@@ -4,3 +4,4 @@ Proof.
 split.
 - exact I.
   Show Proof. (* Was not finding an evar name at some time *)
+Abort.
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 75b66e463a..fa12f09a46 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -21,3 +21,4 @@ Proof.
 intros H.
 Fail intros [H%myid ?].
 Fail destruct 1 as [H%myid ?].
+Abort.
diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v
index d38e2a50e4..2e4008ae56 100644
--- a/test-suite/output/TypeclassDebug.v
+++ b/test-suite/output/TypeclassDebug.v
@@ -6,3 +6,4 @@ Hint Resolve H : foo.
 Goal foo.
 Typeclasses eauto := debug.
 Fail typeclasses eauto 5 with foo.
+Abort.
diff --git a/test-suite/output/names.v b/test-suite/output/names.v
index f1efd0df2a..e9033bd732 100644
--- a/test-suite/output/names.v
+++ b/test-suite/output/names.v
@@ -7,3 +7,4 @@ Fail Definition b y : {x:nat|x=y} := a y.
 Goal (forall n m, n <= m -> m <= n -> n = m) -> True.
 intro H; epose proof (H _ 3) as H.
 Show.
+Abort.
diff --git a/test-suite/output/optimize_heap.v b/test-suite/output/optimize_heap.v
index e566bd7bab..31b4510397 100644
--- a/test-suite/output/optimize_heap.v
+++ b/test-suite/output/optimize_heap.v
@@ -5,3 +5,4 @@ Goal True.
   Show.
   optimize_heap.
   Show.
+Abort.
diff --git a/test-suite/output/rewrite_2172.v b/test-suite/output/rewrite_2172.v
index 212b1c1259..864fc21cdd 100644
--- a/test-suite/output/rewrite_2172.v
+++ b/test-suite/output/rewrite_2172.v
@@ -19,3 +19,4 @@ Proof.
    user in rewrite/induction/destruct calls).
 *)
   Fail rewrite <- axiom.
+Abort.
diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v
index 6424fe92dd..ca93c8ea79 100644
--- a/test-suite/success/CaseInClause.v
+++ b/test-suite/success/CaseInClause.v
@@ -20,6 +20,7 @@ Theorem foo : forall (n m : nat) (pf : n = m),
                 match pf in _ = N with 
                   | eq_refl => unit
                 end.
+Abort.
 
 (* Check redundant clause is removed *)
 Inductive I : nat * nat -> Type := C : I (0,0).
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index 9a19b595ef..b16e4a1186 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -27,6 +27,7 @@ Parameters (a:_) (b:a=0).
 Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.
 
 Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
+Abort.
 
 (* Some example which should succeed with local implicit arguments *)
 
diff --git a/test-suite/success/Print.v b/test-suite/success/Print.v
index c4726bf3ff..c1cb86caf1 100644
--- a/test-suite/success/Print.v
+++ b/test-suite/success/Print.v
@@ -17,3 +17,4 @@ Print Coercion Paths nat Sortclass.
 
 Print Section A.
 
+End A.
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index 2da630633d..06697af901 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -25,4 +25,4 @@ Definition c := ε : U.
 
 Goal True.
 assert (nat * nat).
-
+Abort.
diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index 241d4eb200..7b972f4ed9 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -18,6 +18,7 @@ Check ι _ ι.
 
 #[program]
 Fixpoint f (n: nat) {wf lt n} : nat := _.
+Reset f.
 
 #[deprecated(since="8.9.0")]
 Ltac foo := foo.
diff --git a/test-suite/success/autorewrite.v b/test-suite/success/autorewrite.v
index 5e9064f8af..71d333d439 100644
--- a/test-suite/success/autorewrite.v
+++ b/test-suite/success/autorewrite.v
@@ -27,3 +27,4 @@ Goal forall y, exists x, y+x = y.
 eexists. autorewrite with base1.
 Fail reflexivity.
 
+Abort.
diff --git a/test-suite/success/change_pattern.v b/test-suite/success/change_pattern.v
index 874abf49f1..104585a720 100644
--- a/test-suite/success/change_pattern.v
+++ b/test-suite/success/change_pattern.v
@@ -32,3 +32,4 @@ clearbody e.
     if this is not the case because the inferred argument does not coincide with
     the one in the considered term. *)
 progress (change (dim (traverse unit a x)) with (dim X) in e).
+Abort.
diff --git a/test-suite/success/rewrite_evar.v b/test-suite/success/rewrite_evar.v
index f7ad261cbb..3bfd3c674a 100644
--- a/test-suite/success/rewrite_evar.v
+++ b/test-suite/success/rewrite_evar.v
@@ -6,3 +6,4 @@ Goal forall (T2 MT1 MT2 : Type) (x : T2) (M2 m2 : MT2) (M1 m1 : MT1) (F : T2 ->
   rewrite (H' _) in *.
   (** The above rewrite should also rewrite in H. *)
   Fail progress rewrite H' in H.
+Abort.
diff --git a/test-suite/success/setoid_unif.v b/test-suite/success/setoid_unif.v
index 912596b4a3..d579911323 100644
--- a/test-suite/success/setoid_unif.v
+++ b/test-suite/success/setoid_unif.v
@@ -25,3 +25,4 @@ Goal forall x, ~ In _ x (t Empty).
 Proof.
 intros x.
 rewrite foo.
+Abort.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index de8aa252b8..72f0d94dea 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -23,3 +23,4 @@ Goal let x := 0 in True.
 intro x.
 Fail (clear x; unfold x).
 Abort.
+End toto.
diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v
index c4a1d7c28f..014f1834a2 100644
--- a/test-suite/success/unidecls.v
+++ b/test-suite/success/unidecls.v
@@ -1,22 +1,22 @@
 Set Printing Universes.
 
-Module unidecls.
+Module decls.
   Universes a b.
-End unidecls.
+End decls.
 
 Universe a.
 
-Constraint a < unidecls.a.
+Constraint a < decls.a.
 
 Print Universes.
 
 (** These are different universes *)
 Check Type@{a}.
-Check Type@{unidecls.a}.
+Check Type@{decls.a}.
 
-Check Type@{unidecls.b}.
+Check Type@{decls.b}.
 
-Fail Check Type@{unidecls.c}.
+Fail Check Type@{decls.c}.
 
 Fail Check Type@{i}.
 Universe foo.