From a76e839e5a86dc45bbe9037fbd782abe0727c7dc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Jul 2017 11:19:34 -0700 Subject: [PATCH] chore(tests/lean/keyword_tactics): fix test output --- tests/lean/keyword_tactics.lean.expected.out | 4 ++++ 1 file changed, 4 insertions(+) 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 : ℕ → ℕ +⊢ ℕ