diff --git a/tests/lean/keyword_tactics.lean.expected.out b/tests/lean/keyword_tactics.lean.expected.out index 755a5f2bdf..b089175ea0 100644 --- a/tests/lean/keyword_tactics.lean.expected.out +++ b/tests/lean/keyword_tactics.lean.expected.out @@ -4,3 +4,7 @@ and ℕ : Type state: ⊢ ℕ → ℕ → ℕ +keyword_tactics.lean:45:15: error: solve1 tactic failed, focused goal has not been solved +state: +f : ℕ → ℕ +⊢ ℕ