From 44bc68bdc6052d6db6017f6104634574eea76740 Mon Sep 17 00:00:00 2001
From: Alex J Best <alex.j.best@gmail.com>
Date: Wed, 4 Oct 2023 01:12:43 +0200
Subject: [PATCH] fix: withLocation should use withMainContext for target
 (#2607)

---
 src/Lean/Elab/Tactic/Location.lean        |  2 +-
 tests/lean/withLocation.lean              | 15 +++++++++++++++
 tests/lean/withLocation.lean.expected.out |  2 ++
 3 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/withLocation.lean
 create mode 100644 tests/lean/withLocation.lean.expected.out

diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean
index 6e9134d16e..6276f584ca 100644
--- a/src/Lean/Elab/Tactic/Location.lean
+++ b/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
diff --git a/tests/lean/withLocation.lean b/tests/lean/withLocation.lean
new file mode 100644
index 0000000000..a0f378575a
--- /dev/null
+++ b/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
diff --git a/tests/lean/withLocation.lean.expected.out b/tests/lean/withLocation.lean.expected.out
new file mode 100644
index 0000000000..e6bba11d86
--- /dev/null
+++ b/tests/lean/withLocation.lean.expected.out
@@ -0,0 +1,2 @@
+t
+withLocation.lean:11:0-11:7: warning: declaration uses 'sorry'