diff --git a/src/Lean/Elab/Tactic/Split.lean b/src/Lean/Elab/Tactic/Split.lean index 0dfc66909843..b5f6444a6201 100644 --- a/src/Lean/Elab/Tactic/Split.lean +++ b/src/Lean/Elab/Tactic/Split.lean @@ -21,12 +21,12 @@ open Meta throwErrorAt stx[2] "'split' tactic failed, select a single target to split" if simplifyTarget then liftMetaTactic fun mvarId => do - let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failures true`" + let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failure true`" return mvarIds else let fvarId ← getFVarId hyps[0]! liftMetaTactic fun mvarId => do - let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failures true`" + let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failure true`" return mvarIds | Location.wildcard => liftMetaTactic fun mvarId => do @@ -34,7 +34,7 @@ open Meta for fvarId in fvarIds do if let some mvarIds ← splitLocalDecl? mvarId fvarId then return mvarIds - let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failures true`" + let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failure true`" return mvarIds end Lean.Elab.Tactic diff --git a/tests/lean/run/4390.lean b/tests/lean/run/4390.lean index 4306f00ae0de..5e10f4c31ca3 100644 --- a/tests/lean/run/4390.lean +++ b/tests/lean/run/4390.lean @@ -11,7 +11,7 @@ termination_by state decreasing_by sorry /-- -error: tactic 'split' failed, consider using `set_option trace.split.failures true` +error: tactic 'split' failed, consider using `set_option trace.split.failure true` state : Nat p : (match h : step state with