From 2f8901d6d01351bcfd8f765ca99e003d3f788d37 Mon Sep 17 00:00:00 2001 From: euprunin Date: Tue, 4 Mar 2025 10:42:17 +0100 Subject: [PATCH] chore: add missing period to `grind` warning message (#7317) Co-authored-by: euprunin --- src/Lean/Elab/Tactic/Grind.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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