fix: missing withContext in simp trace (#2053)

As [reported on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.3F.20.5B*.5D/near/322724789).

---------

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/Lean/Elab/Tactic/Simp.lean

@@ -283,7 +283,7 @@ def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do
     | .fvar fvarId => -- local hypotheses in the context
       if let some ldecl := lctx.find? fvarId then
         localsOrStar := localsOrStar.bind fun locals =>
-          if !ldecl.userName.isInaccessibleUserName &&
+          if !ldecl.userName.isInaccessibleUserName && !ldecl.userName.hasMacroScopes &&
               (lctx.findFromUserName? ldecl.userName).get!.fvarId == ldecl.fvarId then
             some (locals.push ldecl.userName)
           else
@@ -337,14 +337,14 @@ where
 /-
   "simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)?
 -/
-@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
-  let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
+@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do
+  let { ctx, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false)
   let usedSimps ← dischargeWrapper.with fun discharge? =>
     simpLocation ctx discharge? (expandOptLocation stx[5])
   if tactic.simp.trace.get (← getOptions) then
     traceSimpCall stx usedSimps
 
-@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => do
+@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do
   let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
   let (result?, usedSimps) ← simpAll (← getMainGoal) ctx
   match result? with
@@ -370,7 +370,7 @@ where
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
     if tactic.simp.trace.get (← getOptions) then
-      traceSimpCall (← getRef) usedSimps
+      mvarId.withContext <| traceSimpCall (← getRef) usedSimps
 
 @[builtin_tactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do
   let { ctx, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)

tests/lean/simp_trace.lean

@@ -134,3 +134,7 @@ example (P Q : Prop) (h : P ↔ Q) (p : P) : Q := by
 theorem my_thm' : a ↔ a ∧ a := my_thm.symm
 
 example (P : Prop) : P ∧ P ↔ P := by simp only [← my_thm']
+
+example {P : Prop} : P → P := by intro h; simp [*]
+
+example {P : Prop} : P → P := by intro; simp [*]

tests/lean/simp_trace.lean.expected.out

@@ -120,3 +120,7 @@ Try this: simp only [← h]
 Try this: simp only [← my_thm']
 [Meta.Tactic.simp.rewrite] ← @my_thm':1000, P ∧ P ==> P
 [Meta.Tactic.simp.rewrite] iff_self:1000, P ↔ P ==> True
+Try this: simp only [h]
+[Meta.Tactic.simp.rewrite] h:1000, P ==> True
+Try this: simp only [*]
+[Meta.Tactic.simp.rewrite] a✝:1000, P ==> True