chore: remove staging workarounds

src/Init/Grind/Tactics.lean

@@ -71,8 +71,8 @@ syntax grindEq     := "=" (grindGen)?
 syntax grindEqBoth := atomic("_" "=" "_") (grindGen)?
 syntax grindEqRhs  := atomic("=" "_") (grindGen)?
 syntax grindEqBwd  := atomic("←" "=") <|> atomic("<-" "=")
-syntax grindBwd    := ("← " <|> "←" <|> "<-") (grindGen)? -- TODO remove "← " after update stage 0
-syntax grindFwd    := "→ " <|> "→" <|> "->" -- TODO remove "→ " after update stage 0
+syntax grindBwd    := ("←" <|> "<-") (grindGen)?
+syntax grindFwd    := "→" <|> "->"
 syntax grindRL     := "⇐" <|> "<="
 syntax grindLR     := "⇒" <|> "=>"
 syntax grindUsr    := &"usr"

src/Lean/Meta/Tactic/Grind/Attr.lean

@@ -42,14 +42,7 @@ def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do
   | `(Parser.Attr.grindMod|cases eager) => return .cases true
   | `(Parser.Attr.grindMod|intro) => return .intro
   | `(Parser.Attr.grindMod|ext) => return .ext
-  | _ =>
-    -- TODO: remove after update stage0
-    let stx := stx[0]
-    if stx.isOfKind ``Parser.Attr.grindFwd then return .ematch .fwd
-    if stx.isOfKind ``Parser.Attr.grindBwd then return .ematch (.bwd false)
-    if stx.isOfKind ``Parser.Attr.grindRL then return .ematch .rightLeft
-    if stx.isOfKind ``Parser.Attr.grindLR then return .ematch .leftRight
-    throwError "unexpected `grind` theorem kind: `{stx}`"
+  | _ => throwError "unexpected `grind` theorem kind: `{stx}`"
 
 /-- Return theorem kind for `stx` of the form `(Attr.grindMod)?` -/
 def getAttrKindFromOpt (stx : Syntax) : CoreM AttrKind := do

tests/lean/run/grind_pp_attr.lean

@@ -25,3 +25,35 @@ example :=
 -/
 #guard_msgs in
 run_cmd test (← `(@[grind _=_] example := 0))
+
+/--
+info: @[grind =_]
+example :=
+  0
+-/
+#guard_msgs in
+run_cmd test (← `(@[grind =_] example := 0))
+
+/--
+info: @[grind →]
+example :=
+  0
+-/
+#guard_msgs in
+run_cmd test (← `(@[grind →] example := 0))
+
+/--
+info: @[grind ←]
+example :=
+  0
+-/
+#guard_msgs in
+run_cmd test (← `(@[grind ←] example := 0))
+
+/--
+info: @[grind ←=]
+example :=
+  0
+-/
+#guard_msgs in
+run_cmd test (← `(@[grind ←=] example := 0))