4 files changed, 8 insertions, 7 deletions
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index efb32ef6f7..81c9763ccd 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -50,8 +50,6 @@ End folding.
 
 (* Check definition by tactics *)
 
-Set Automatic Introduction.
-
 Inductive even : nat -> Type :=
   | even_O : even 0
   | even_S : forall n, odd n -> even (S n)
diff --git a/test-suite/success/Require.v b/test-suite/success/Require.v
index f851d8c7d9..de5987c4f7 100644
--- a/test-suite/success/Require.v
+++ b/test-suite/success/Require.v
@@ -1,3 +1,8 @@
+(* -*- coq-prog-args: ("-noinit"); -*- *)
+
 Require Import Coq.Arith.Plus.
 Require Coq.Arith.Minus.
 Locate Library Coq.Arith.Minus.
+
+(* Check that Init didn't get exported by the import above *)
+Fail Check nat.
diff --git a/test-suite/success/autointros.v b/test-suite/success/autointros.v
index 0a0812711c..1140a537fc 100644
--- a/test-suite/success/autointros.v
+++ b/test-suite/success/autointros.v
@@ -1,5 +1,3 @@
-Set Automatic Introduction.
-
 Inductive even : nat -> Prop :=
 | even_0 : even 0
 | even_odd : forall n, odd n -> even (S n)
diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v
index 7c298c98b6..1bc565cbb5 100644
--- a/test-suite/success/unidecls.v
+++ b/test-suite/success/unidecls.v
@@ -1,4 +1,4 @@
-(* coq-prog-args: ("-top" "unidecls") *)
+(* -*- coq-prog-args: ("-top" "unidecls"); -*- *)
 Set Printing Universes.
 
 Module decls.
@@ -46,12 +46,12 @@ Universe secfoo.
 Section Foo'.
   Fail Universe secfoo.
   Universe secfoo2.
-  Check Type@{Foo'.secfoo2}.
+  Fail Check Type@{Foo'.secfoo2}.
+  Check Type@{secfoo2}.
   Constraint secfoo2 < a.
 End Foo'.
 
 Check Type@{secfoo2}.
-Fail Check Type@{Foo'.secfoo2}.
 Fail Check eq_refl : Type@{secfoo2} = Type@{a}.
 
 (** Below, u and v are global, fixed universes *)