5 files changed, 1 insertions, 5 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.