Merge PR #8630: Some cleaning in the test suite

16 files changed, 20 insertions, 11 deletions

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/Cases-bug1834.v b/test-suite/success/Cases_bug1834.v
index cf102486a6..65372c2da4 100644
--- a/test-suite/success/Cases-bug1834.v
+++ b/test-suite/success/Cases_bug1834.v
@@ -10,4 +10,3 @@ Parameter a : U.
 Check (match a with exist _ (exist _ tt e2) e3 => e3=e3 end).
 
 (* There is still a form submitted by Pierre Corbineau (#1834) which fails *)
-
diff --git a/test-suite/success/Cases-bug3758.v b/test-suite/success/Cases_bug3758.v
index e48f452326..e48f452326 100644
--- a/test-suite/success/Cases-bug3758.v
+++ b/test-suite/success/Cases_bug3758.v
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/all-check.v b/test-suite/success/all_check.v
index 391bc540e4..391bc540e4 100644
--- a/test-suite/success/all-check.v
+++ b/test-suite/success/all_check.v
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/dtauto-let-deps.v b/test-suite/success/dtauto_let_deps.v
index 094b2f8b3c..094b2f8b3c 100644
--- a/test-suite/success/dtauto-let-deps.v
+++ b/test-suite/success/dtauto_let_deps.v
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..7c298c98b6 100644
--- a/test-suite/success/unidecls.v
+++ b/test-suite/success/unidecls.v
@@ -1,22 +1,23 @@
+(* coq-prog-args: ("-top" "unidecls") *)
 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.
@@ -39,7 +40,7 @@ Check Type@{Foo.bar}.
 Check Type@{Foo.foo}.
 (** The same *)
 Check Type@{foo}.
-Check Type@{Top.foo}.
+Check Type@{unidecls.foo}.
 
 Universe secfoo.
 Section Foo'.
diff --git a/test-suite/success/universes-coercion.v b/test-suite/success/universes_coercion.v
index d750434027..272d3ec74a 100644
--- a/test-suite/success/universes-coercion.v
+++ b/test-suite/success/universes_coercion.v
@@ -5,7 +5,7 @@
    of universe polymorphism obsolete (example submitted by Randy Pollack).
 
    Note that this example is not an evidence that the current
-   non-kernel eta-expansion behavior is the most expected one.  
+   non-kernel eta-expansion behavior is the most expected one.
 *)
 
 Parameter K : forall T : Type, T -> T.
@@ -14,7 +14,7 @@ Check (K (forall T : Type, T -> T) K).
 (*
    note that the inferred term is
      "(K (forall T (* u1 *) : Type, T -> T) (fun T:Type (* u1 *) => K T))"
-   which is not eta-equivalent to 
+   which is not eta-equivalent to
      "(K (forall T : Type, T -> T) K"
    because the eta-expansion of the latter
      "(K (forall T : Type, T -> T) (fun T:Type (* u2 *) => K T)"