From 875e71a0d704c7d7148e507a283484fc08c4431f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Jun 2022 18:24:10 -0700 Subject: [PATCH] chore: unused variables at `Simp.lean` --- src/Lean/Elab/Tactic/Simp.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 29ddb0c930..19727aafd7 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -287,17 +287,17 @@ where | none => replaceMainGoal [] | some mvarId => replaceMainGoal [mvarId] -def dsimpLocation (ctx : Simp.Context) (fvarIdToSimp : FVarIdToLemmaId := {}) (loc : Location) : TacticM Unit := do +def dsimpLocation (ctx : Simp.Context) (loc : Location) : TacticM Unit := do match loc with | Location.targets hyps simplifyTarget => withMainContext do let fvarIds ← getFVarIds hyps - go fvarIds simplifyTarget fvarIdToSimp + go fvarIds simplifyTarget | Location.wildcard => withMainContext do - go (← getNondepPropHyps (← getMainGoal)) (simplifyTarget := true) fvarIdToSimp + go (← getNondepPropHyps (← getMainGoal)) (simplifyTarget := true) where - go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) (fvarIdToSimp : Lean.Meta.FVarIdToLemmaId) : TacticM Unit := do + go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Unit := do let mvarId ← getMainGoal let result? ← dsimpGoal mvarId ctx (simplifyTarget := simplifyTarget) (fvarIdsToSimp := fvarIdsToSimp) match result? with @@ -305,7 +305,7 @@ where | some mvarId => replaceMainGoal [mvarId] @[builtinTactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do - let { ctx, fvarIdToLemmaId, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp) - dsimpLocation ctx fvarIdToLemmaId (expandOptLocation stx[5]) + let { ctx, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp) + dsimpLocation ctx (expandOptLocation stx[5]) end Lean.Elab.Tactic