From 94ecc3292fea718e794f53ba6d7f8c57722495d8 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 20 Jul 2017 22:51:42 +0100 Subject: [PATCH] fix(tests): fix tests --- tests/lean/andthen_focus_error_message.lean.expected.out | 6 ++---- tests/lean/interactive/focus.lean.expected.out | 2 +- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/tests/lean/andthen_focus_error_message.lean.expected.out b/tests/lean/andthen_focus_error_message.lean.expected.out index c2f42ab865..6189cb07a0 100644 --- a/tests/lean/andthen_focus_error_message.lean.expected.out +++ b/tests/lean/andthen_focus_error_message.lean.expected.out @@ -8,11 +8,9 @@ a b c : ℕ ⊢ b = b andthen_focus_error_message.lean:16:14: error: focus tactic failed, insufficient number of tactics state: -no goals +a : ℕ +⊢ a = a andthen_focus_error_message.lean:22:14: error: focus tactic failed, insufficient number of tactics state: a : ℕ ⊢ a = a - -a : ℕ -⊢ a = a diff --git a/tests/lean/interactive/focus.lean.expected.out b/tests/lean/interactive/focus.lean.expected.out index 5a7f3c6d63..fafa3fc0ef 100644 --- a/tests/lean/interactive/focus.lean.expected.out +++ b/tests/lean/interactive/focus.lean.expected.out @@ -1,4 +1,4 @@ -{"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":4,"severity":"error","text":"focus tactic failed, insufficient number of tactics\nstate:\nb c : ℕ,\na_2 : b = 0\n⊢ b = 0"}],"response":"all_messages"} +{"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":4,"severity":"error","text":"focus tactic failed, insufficient number of tactics\nstate:\na b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ b = a"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} {"record":{"source":,"state":"a b c : ℕ,\na_1 : a = b,\na_2 : b = 0\n⊢ a = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":5} {"record":{"source":,"state":"b c : ℕ,\na_2 : b = 0\n⊢ b = 0","tactic_param_idx":0,"tactic_params":["{ tactic }"],"text":"focus","type":"tactic.interactive.itactic → tactic unit"},"response":"ok","seq_num":7}