diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 776b43432d..e2d30ff0b8 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1994,9 +1994,12 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved
 where
   process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
     if candidates.isEmpty then
+      let env ← getEnv
       if (← read).autoBoundImplicit &&
            !(← read).autoBoundImplicitForbidden n &&
-           isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) then
+           isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) &&
+           -- do not turn a scope error into an auto implicit
+           !(env.isExporting && (env.setExporting false).contains n) then
         throwAutoBoundImplicitLocal n
       else
         throwUnknownIdentifierAt (declHint := n) stx m!"Unknown identifier `{.ofConstName n}`"
diff --git a/tests/pkg/module/Module/PrivateImported.lean b/tests/pkg/module/Module/PrivateImported.lean
index 0715b4e9d8..9ce7f30e91 100644
--- a/tests/pkg/module/Module/PrivateImported.lean
+++ b/tests/pkg/module/Module/PrivateImported.lean
@@ -12,7 +12,6 @@ error: Unknown identifier `f`
 Note: A private declaration `f` exists but is not accessible in the current context.
 -/
 #guard_msgs in
-set_option autoImplicit false in
 public theorem t2 : f = 1 := sorry
 
 /--