diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index f3004385e8..7df86d5fce 100644
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@@ -192,7 +192,7 @@ syntax (name := exposeNames) "expose_names" : grind
 /--
 `set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,
 but it sets the option only within the tactics `tacs`. -/
-syntax (name := setOption) "set_option " ident ppSpace optionValue " in " grindSeq : grind
+syntax (name := setOption) "set_option " (ident (noWs "." noWs ident)?) ppSpace optionValue " in " grindSeq : grind
 
 end Grind
 end Lean.Parser.Tactic
diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
index d6f95f3665..36f3d11162 100644
--- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
@@ -426,7 +426,7 @@ where
   replaceMainGoal [{ goal with mvarId }]
 
 @[builtin_grind_tactic setOption] def elabSetOption : GrindTactic := fun stx => do
-  let options ← Elab.elabSetOption stx[1] stx[2]
-  withOptions (fun _ => options) do evalGrindTactic stx[4]
+  let options ← Elab.elabSetOption stx[1] stx[3]
+  withOptions (fun _ => options) do evalGrindTactic stx[5]
 
 end Lean.Elab.Tactic.Grind