test-suite: cleaning

12 files changed, 15 insertions, 0 deletions

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.