Misleading `simp` mention in `cbv` error message

[juanjomadrigal]

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.