fix: withLocation should use withMainContext for target (#2607)

src/Lean/Elab/Tactic/Location.lean

@@ -49,7 +49,7 @@ def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget
       let fvarId ← getFVarId hyp
       atLocal fvarId
     if type then
-      atTarget
+      withMainContext atTarget
   | Location.wildcard =>
     let worked ← tryTactic <| withMainContext <| atTarget
     withMainContext do

tests/lean/withLocation.lean

@@ -0,0 +1,15 @@
+import Lean
+
+open Lean Elab Tactic
+elab "test" : tactic => do
+  withLocation (.targets #[] true) (fun _ => return ())
+    do
+      let some (_, lhs, _) := (← getMainTarget).eq? | failure
+      logInfo <| ← FVarId.getUserName (lhs.fvarId!)
+    (fun _ => return ())
+
+example : 1 = 1 := by
+  let t := 1
+  show t = 1
+  test
+  sorry

tests/lean/withLocation.lean.expected.out

@@ -0,0 +1,2 @@
+t
+withLocation.lean:11:0-11:7: warning: declaration uses 'sorry'