chore: use realizeGlobalConstNoOverloadWithInfo

closes #10427 closes #10426
2026-03-27 23:34:11 +00:00 · 2025-10-25 19:35:33 -07:00
1 changed files with 1 additions and 2 deletions
--- a/src/Lean/Elab/Tactic/Grind/Main.lean
+++ b/src/Lean/Elab/Tactic/Grind/Main.lean
@@ -35,8 +35,7 @@ def elabGrindPattern : CommandElab := fun stx => do
  | _ => throwUnsupportedSyntax
 where
  go (thmName : TSyntax `ident) (terms : Syntax.TSepArray `term ",") (kind : AttributeKind) : CommandElabM Unit := liftTermElabM do
-    let declName ← resolveGlobalConstNoOverload thmName
-    discard <| addTermInfo thmName (← mkConstWithLevelParams declName)
+    let declName ← realizeGlobalConstNoOverloadWithInfo thmName
    let info ← getConstVal declName
    forallTelescope info.type fun xs _ => do
      let patterns ← terms.getElems.mapM fun term => do