doc: fix option name

2026-04-10 06:04:09 +00:00 · 2024-08-24 18:28:52 -04:00
1 changed files with 1 additions and 1 deletions
--- a/src/Lean/Elab/AutoBound.lean
+++ b/src/Lean/Elab/AutoBound.lean
@@ -17,7 +17,7 @@ register_builtin_option autoImplicit : 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`."
+    descr    := "When \"relaxed\" mode is enabled, any atomic nonempty identifier is eligible for auto bound implicit locals (see option `autoImplicit`)."
  }