diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index 7e802118a6..da4b8060a9 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -167,7 +167,7 @@ def evalGrindCore let only := only.isSome let params := if let some params := params then params.getElems else #[] if Grind.grind.warning.get (← getOptions) then - logWarningAt ref "The `grind` tactic is experimental and still under development. Avoid using it in production projects" + logWarningAt ref "The `grind` tactic is experimental and still under development. Avoid using it in production projects." let declName := (← Term.getDeclName?).getD `_grind withMainContext do let result ← grind (← getMainGoal) config only params declName fallback