From c9708e7bd7cf47106e2fc063d3c586c8f333e54d Mon Sep 17 00:00:00 2001
From: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Date: Sun, 22 Mar 2026 12:54:33 -0400
Subject: [PATCH] doc: update docstring of `Lean.Parser.Tactic.Grind.first`
 (#12998)

This PR updates the docstring for `Lean.Parser.Tactic.Grind.first`,
which changed syntax in #10828.
---
 src/Init/Grind/Interactive.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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. -/