From 458eed730fee0785301a97a0f53bd04c39e4c33c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 21 Jan 2020 11:16:04 +0100 Subject: [PATCH] chore: fix confusing indentation --- src/Init/Lean/Elab/Tactic/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Elab/Tactic/Basic.lean b/src/Init/Lean/Elab/Tactic/Basic.lean index cd475587af..05759532a3 100644 --- a/src/Init/Lean/Elab/Tactic/Basic.lean +++ b/src/Init/Lean/Elab/Tactic/Basic.lean @@ -177,7 +177,7 @@ partial def evalTactic : Syntax → TacticM Unit -- Syntax quotations can return multiple ones stx.forSepArgsM evalTactic else do - trace `Elab.step stx $ fun _ => stx; + trace `Elab.step stx $ fun _ => stx; s ← get; let table := (tacticElabAttribute.ext.getState s.env).table; let k := stx.getKind;