From 0e01d855b075311191517936dfca272d69f627c7 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 16 Sep 2022 14:43:19 +0200 Subject: [PATCH] chore: fix test --- tests/lean/traceTacticSteps.lean.expected.out | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/tests/lean/traceTacticSteps.lean.expected.out b/tests/lean/traceTacticSteps.lean.expected.out index 3182ab4751..a918e39a43 100644 --- a/tests/lean/traceTacticSteps.lean.expected.out +++ b/tests/lean/traceTacticSteps.lean.expected.out @@ -18,17 +18,14 @@ [Elab.step] focus apply And.intro✝ with_annotate_state"<;>" skip - all_goals - trivial + all_goals trivial [Elab.step] apply And.intro✝ with_annotate_state"<;>" skip - all_goals - trivial + all_goals trivial [Elab.step] apply And.intro✝ with_annotate_state"<;>" skip - all_goals - trivial + all_goals trivial [Elab.step] apply And.intro✝ [Elab.step] apply True.intro✝