Misleading `simp` mention in `cbv` error message

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

simp being mentioned instead of cbv in a failing tactic execution.

Context

Newly introduced cbv tactic

Steps to Reproduce

A simple code like

def fact : Nat → Nat
| 0 => 1
| n+1 => (n+1) * fact n

set_option cbv.maxSteps 20 in
example : fact 5 > 0 := by
  cbv

generates a somewhat misleading message involving simp (it should be cbv)

`simp` failed: maximum number of steps exceeded

Expected behavior: `cbv` failed: maximum number of steps exceeded

Actual behavior: `simp` failed: maximum number of steps exceeded

Versions

4.30.0-rc2/ 4.31.0-nightly-2026-05-12

Impact

Low

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal fact example with set_option cbv.maxSteps 20 and search the tactic implementation for the exact simp failure text. Update the error wording so this cbv invocation reports cbv, then rerun the reproduction and confirm the message matches the expected behavior.