diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index 64fa3d46ad..a9f2ef9ed2 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -182,7 +182,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 new and its behaviour may change in the future. This project has used `set_option grind.warning true` to discourage its use." withMainContext do let result ← grind (← getMainGoal) config only params fallback replaceMainGoal [] diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 6479a84126..820a1d17d1 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -48,9 +48,9 @@ register_builtin_option grind.debug.proofs : Bool := { } register_builtin_option grind.warning : Bool := { - defValue := true + defValue := false group := "debug" - descr := "disable `grind` usage warning" + descr := "generate a warning whenever `grind` is used" } /--