diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean index 809c8c9d94..98f218f038 100644 --- a/src/Lean/Elab/Tactic/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Rewrite.lean @@ -50,7 +50,6 @@ def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx => do let loc := expandOptLocation stx[2] -- show initial state up to (incl.) `[` withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ()) - let mut newTacs := #[] let numRules := (rules.size + 1) / 2 for i in [:numRules] do let rule := rules[i * 2]