11 files changed, 21 insertions, 11 deletions
diff --git a/test-suite/bugs/closed/bug_2001.v b/test-suite/bugs/closed/bug_2001.v
index 652c65706a..31c62b7b36 100644
--- a/test-suite/bugs/closed/bug_2001.v
+++ b/test-suite/bugs/closed/bug_2001.v
@@ -1,12 +1,10 @@
 (* Automatic computing of guard in "Theorem with"; check that guard is not
    computed when the user explicitly indicated it *)
 
-Unset Automatic Introduction.
-
 Inductive T : Set :=
 | v : T.
 
-Definition f (s:nat) (t:T) : nat.
+Definition f : forall (s:nat) (t:T), nat.
 fix f 2.
 intros s t.
 refine
diff --git a/test-suite/bugs/closed/gh6165.v b/test-suite/bugs/closed/bug_6165.v
index b87a7caaf2..b87a7caaf2 100644
--- a/test-suite/bugs/closed/gh6165.v
+++ b/test-suite/bugs/closed/bug_6165.v
diff --git a/test-suite/bugs/closed/gh6384.v b/test-suite/bugs/closed/bug_6384.v
index cec84642fb..cec84642fb 100644
--- a/test-suite/bugs/closed/gh6384.v
+++ b/test-suite/bugs/closed/bug_6384.v
diff --git a/test-suite/bugs/closed/gh6385.v b/test-suite/bugs/closed/bug_6385.v
index 3bbb664f4f..3bbb664f4f 100644
--- a/test-suite/bugs/closed/gh6385.v
+++ b/test-suite/bugs/closed/bug_6385.v
diff --git a/test-suite/bugs/closed/bug_6661.v b/test-suite/bugs/closed/bug_6661.v
index e88a3704d8..28a9ffc7bd 100644
--- a/test-suite/bugs/closed/bug_6661.v
+++ b/test-suite/bugs/closed/bug_6661.v
@@ -53,8 +53,6 @@ Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X.
   exact x.
 Defined.
 
-Unset Automatic Introduction.
-
 Definition idfun (T : UU) := λ t:T, t.
 
 Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c.
diff --git a/test-suite/output/PrintUnivsSubgraph.out b/test-suite/output/PrintUnivsSubgraph.out
new file mode 100644
index 0000000000..c42e15e4e8
--- /dev/null
+++ b/test-suite/output/PrintUnivsSubgraph.out
@@ -0,0 +1,5 @@
+Prop < Set
+Set < i
+    < j
+i < j
+
diff --git a/test-suite/output/PrintUnivsSubgraph.v b/test-suite/output/PrintUnivsSubgraph.v
new file mode 100644
index 0000000000..ec9cf44d4f
--- /dev/null
+++ b/test-suite/output/PrintUnivsSubgraph.v
@@ -0,0 +1,9 @@
+
+Universes i j k l.
+
+Definition foo : Type@{j} := Type@{i}.
+
+Definition baz : Type@{k} := Type@{l}.
+
+Print Universes Subgraph(i j).
+(* should print [i < j], not [l < k] (and not prelude universes) *)
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index d63b6dbfce..4d3f7419e6 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -41,8 +41,7 @@ Arguments A, Wrap are implicit and maximally inserted
 Argument scopes are [type_scope _]
 Polymorphic bar@{u} = nat
      : Wrap@{u} Set
-(* u |= Set < u
-         *)
+(* u |= Set < u *)
 
 bar is universe polymorphic
 Polymorphic foo@{u UnivBinders.17 v} = 
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)