diff --git a/RELEASES.md b/RELEASES.md
index 6dc5a6cc4c..c44d1eb64a 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -22,4 +22,6 @@ theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)]
 
 * Auto generated congruence lemmas with support for casts on proofs and `Decidable` instances (see [whishlist](https://github.com/leanprover/lean4/issues/988)).
 
-* [Relax auto-implicit restrictions](https://github.com/leanprover/lean4/pull/1011). The command `set_option relaxedAutoBoundImplicitLocal false` disables the relaxations.
+* Rename option `autoBoundImplicitLocal` => `autoImplicit`.
+
+* [Relax auto-implicit restrictions](https://github.com/leanprover/lean4/pull/1011). The command `set_option relaxedAutoImplicit false` disables the relaxations.
diff --git a/src/Lean/Elab/AutoBound.lean b/src/Lean/Elab/AutoBound.lean
index 6ca3c93434..6f6d9f90c6 100644
--- a/src/Lean/Elab/AutoBound.lean
+++ b/src/Lean/Elab/AutoBound.lean
@@ -9,12 +9,12 @@ import Lean.Data.Options
 
 namespace Lean.Elab
 
-register_builtin_option autoBoundImplicitLocal : Bool := {
+register_builtin_option autoImplicit : Bool := {
     defValue := true
     descr    := "Unbound local variables in declaration headers become implicit arguments. In \"relaxed\" mode (default), any atomic identifier is eligible, otherwise only a lower case or greek letter followed by numeric digits are eligible. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}."
   }
 
-register_builtin_option relaxedAutoBoundImplicitLocal : Bool := {
+register_builtin_option relaxedAutoImplicit : Bool := {
     defValue := true
     descr    := "When \"relaxed\" mode is enabled, any atomic nonempty identifier is eligible for auto bound implicit locals (see optin `autoBoundImplicitLocal`."
   }
diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean
index cbeb9dd9cf..5f41bd5b10 100644
--- a/src/Lean/Elab/Level.lean
+++ b/src/Lean/Elab/Level.lean
@@ -72,7 +72,7 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
   else if kind == identKind then
     let paramName := stx.getId
     unless (← get).levelNames.contains paramName do
-      if (← read).autoBoundImplicit && isValidAutoBoundLevelName paramName (relaxedAutoBoundImplicitLocal.get (← read).options) then
+      if (← read).autoBoundImplicit && isValidAutoBoundLevelName paramName (relaxedAutoImplicit.get (← read).options) then
         modify fun s => { s with levelNames := paramName :: s.levelNames }
       else
         throwError "unknown universe level '{paramName}'"
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 8c2b4b98fc..866ede26d1 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1297,7 +1297,7 @@ def elabType (stx : Syntax) : TermElabM Expr := do
   Enable auto-bound implicits, and execute `k` while catching auto bound implicit exceptions. When an exception is caught,
   a new local declaration is created, registered, and `k` is tried to be executed again. -/
 partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
-  let flag := autoBoundImplicitLocal.get (← getOptions)
+  let flag := autoImplicit.get (← getOptions)
   if flag then
     withReader (fun ctx => { ctx with autoBoundImplicit := flag, autoBoundImplicits := {} }) do
       let rec loop (s : SavedState) : TermElabM α := do
@@ -1418,7 +1418,7 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List Stri
     throw ex
 where process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
   if candidates.isEmpty then
-    if (← read).autoBoundImplicit && isValidAutoBoundImplicitName n (relaxedAutoBoundImplicitLocal.get (← getOptions)) then
+    if (← read).autoBoundImplicit && isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) then
       throwAutoBoundImplicitLocal n
     else
       throwError "unknown identifier '{Lean.mkConst n}'"
diff --git a/tests/lean/1011.lean b/tests/lean/1011.lean
index 2bcd79eceb..4c5357e347 100644
--- a/tests/lean/1011.lean
+++ b/tests/lean/1011.lean
@@ -1,5 +1,5 @@
 def f (x : A) := x
 
-set_option relaxedAutoBoundImplicitLocal false
+set_option relaxedAutoImplicit false
 
 def g (x : A) := x
diff --git a/tests/lean/autoBoundImplicits1.lean b/tests/lean/autoBoundImplicits1.lean
index 18f22fdd07..7352980ebf 100644
--- a/tests/lean/autoBoundImplicits1.lean
+++ b/tests/lean/autoBoundImplicits1.lean
@@ -1,5 +1,5 @@
 def myid (a : α) := a -- works
-set_option relaxedAutoBoundImplicitLocal false
+set_option relaxedAutoImplicit false
 #check myid 10
 #check myid true
 
@@ -20,7 +20,7 @@ def Vec.map (xs : Vec α n) (f : α → β) : Vec β n :=
 def Vec.map2 (xs : Vec α size /- error: unknown identifier size -/) (f : α → β) : Vec β n :=
   ⟨ xs.val.map f, sorry ⟩
 
-set_option autoBoundImplicitLocal false in
+set_option autoImplicit false in
 def Vec.map3 (xs : Vec α n) (f : α → β) : Vec β n := -- Errors, unknown identifiers 'α', 'n', 'β'
   ⟨ xs.val.map f, sorry ⟩
 
diff --git a/tests/lean/autoBoundImplicits2.lean b/tests/lean/autoBoundImplicits2.lean
index 50fbab44b1..9336684fc9 100644
--- a/tests/lean/autoBoundImplicits2.lean
+++ b/tests/lean/autoBoundImplicits2.lean
@@ -1,6 +1,6 @@
 def f [Add α] (a : α) : α :=
   a + a
-set_option relaxedAutoBoundImplicitLocal false
+set_option relaxedAutoImplicit false
 def BV (n : Nat) := { a : Array Bool // a.size = n }
 
 def allZero (bv : BV n) : Prop :=
@@ -26,7 +26,7 @@ def g1 {α : Type u} (a : α) : α :=
 
 #check g1
 
-set_option autoBoundImplicitLocal false in
+set_option autoImplicit false in
 def g2 {α : Type u /- Error -/} (a : α) : α :=
   a
 
diff --git a/tests/lean/doSeqRightIssue.lean b/tests/lean/doSeqRightIssue.lean
index 00f580ec79..b050dd9450 100644
--- a/tests/lean/doSeqRightIssue.lean
+++ b/tests/lean/doSeqRightIssue.lean
@@ -1,5 +1,5 @@
 --
-set_option autoBoundImplicitLocal false
+set_option autoImplicit false
 universe u
 variable {α : Type u}
 variable {β : α → Type v}
diff --git a/tests/lean/interactive/533.lean b/tests/lean/interactive/533.lean
index b247d296ea..8f2cbf6083 100644
--- a/tests/lean/interactive/533.lean
+++ b/tests/lean/interactive/533.lean
@@ -1,4 +1,4 @@
-set_option relaxedAutoBoundImplicitLocal false
+set_option relaxedAutoImplicit false
 inductive Foo where
  | bar : F
         --^ textDocument/completion
diff --git a/tests/lean/interactive/hoverException.lean b/tests/lean/interactive/hoverException.lean
index bf24cf1079..3a978bf8cb 100644
--- a/tests/lean/interactive/hoverException.lean
+++ b/tests/lean/interactive/hoverException.lean
@@ -1,4 +1,4 @@
-set_option relaxedAutoBoundImplicitLocal false
+set_option relaxedAutoImplicit false
 inductive Foo
 | mk : (a b : Bar) → Foo
             --^ textDocument/hover
diff --git a/tests/lean/run/ctorAutoParams.lean b/tests/lean/run/ctorAutoParams.lean
index 5207e4c089..f8b6aa964c 100644
--- a/tests/lean/run/ctorAutoParams.lean
+++ b/tests/lean/run/ctorAutoParams.lean
@@ -25,7 +25,7 @@ inductive Bigstep : Command × State → State → Nat → Prop where
 
 namespace WithoutAutoImplicit
 
-set_option autoBoundImplicitLocal false
+set_option autoImplicit false
 
 inductive Bigstep : Command × State → State → Nat → Prop where
   | skip    {σ} : Bigstep (skip, σ) σ 1
diff --git a/tests/lean/structSorryBug.lean b/tests/lean/structSorryBug.lean
index fea977b680..c2c53213c4 100644
--- a/tests/lean/structSorryBug.lean
+++ b/tests/lean/structSorryBug.lean
@@ -1,4 +1,4 @@
-set_option relaxedAutoBoundImplicitLocal false
+set_option relaxedAutoImplicit false
 instance has_arr : HasArr Preorder := { Arr := Function }
 
 def foo : Nat := { first := 10 }