From 31d2c8fb66aa14048017030d77c80bac36843207 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 27 Oct 2022 18:57:25 -0700 Subject: [PATCH] chore: fix test --- tests/lean/traceTacticSteps.lean.expected.out | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/tests/lean/traceTacticSteps.lean.expected.out b/tests/lean/traceTacticSteps.lean.expected.out index a918e39a43..cd52c46bd9 100644 --- a/tests/lean/traceTacticSteps.lean.expected.out +++ b/tests/lean/traceTacticSteps.lean.expected.out @@ -6,13 +6,13 @@ skip trivial [Elab.step.result] ?m +[Elab.step] + skip + trivial +[Elab.step] + skip + trivial [Elab.step] skip -[Elab.step] - skip - trivial -[Elab.step] - skip - trivial [Elab.step] trivial [Elab.step] (apply And.intro✝) <;> trivial [Elab.step] focus