diff --git a/src/Init/Grind/Interactive.lean b/src/Init/Grind/Interactive.lean
index 77bb6e67e1..94bd71023d 100644
--- a/src/Init/Grind/Interactive.lean
+++ b/src/Init/Grind/Interactive.lean
@@ -205,7 +205,7 @@ macro:1 x:grind tk:" <;> " y:grind:2 : grind => `(grind|
     with_annotate_state $tk skip
     all_goals $y:grind)
 
-/-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
+/-- `first (tac) ...` runs each `tac` until one succeeds, or else fails. -/
 syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "(" grindSeq ")")+) : grind
 
 /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/