From 8bba335f6993c94530a3e2ab5add02cb23d67d0f Mon Sep 17 00:00:00 2001
From: Joe Hendrix <joe@lean-fro.org>
Date: Tue, 20 Feb 2024 22:45:15 -0800
Subject: [PATCH] chore: fix symm and label bugs from #3408

---
 src/Init/Meta.lean             | 18 ------------------
 src/Init/Tactics.lean          |  2 +-
 src/Lean/Elab/Tactic/Symm.lean |  5 +++--
 src/Lean/LabelAttribute.lean   | 14 ++++++++++++++
 4 files changed, 18 insertions(+), 21 deletions(-)

diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 8d4850c31e28..84c7b2746bf3 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -1429,24 +1429,6 @@ declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " fun (c : Lean
 
 end Tactic
 
-namespace Command
-
-/--
-Initialize a new "label" attribute.
-Declarations tagged with the attribute can be retrieved using `Std.Tactic.LabelAttr.labelled`.
--/
-macro (name := _root_.Lean.Parser.Command.registerLabelAttr)
-  doc:(docComment)? "register_label_attr " id:ident : command => do
-  let str := id.getId.toString
-  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
-  let descr := quote (removeLeadingSpaces
-    (doc.map (·.getDocString) |>.getD ("labelled declarations for " ++ id.getId.toString)))
-  `($[$doc:docComment]? initialize ext : LabelExtension ←
-      registerLabelAttr $(quote id.getId) $descr $(quote id.getId)
-    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str : attr)
-
-end Command
-
 end Parser
 
 end Lean
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 621f98580c52..ed4dba5b49b4 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1167,7 +1167,7 @@ syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command
   It replaces the target with `u ~ t`.
 * `symm at h` will rewrite a hypothesis `h : t ~ u` to `h : u ~ t`.
 -/
-syntax (name := symm) "symm" (Parser.Tactic.location)? : tactic
+syntax (name := symm) "symm" (location)? : tactic
 
 /-- For every hypothesis `h : a ~ b` where a `@[symm]` lemma is available,
 add a hypothesis `h_symm : b ~ a`. -/
diff --git a/src/Lean/Elab/Tactic/Symm.lean b/src/Lean/Elab/Tactic/Symm.lean
index 2017561f2987..263a8dd17962 100644
--- a/src/Lean/Elab/Tactic/Symm.lean
+++ b/src/Lean/Elab/Tactic/Symm.lean
@@ -12,10 +12,11 @@ namespace Lean.Elab.Tactic
 @[builtin_tactic Lean.Parser.Tactic.symm]
 def evalSymm : Tactic := fun stx =>
   match stx with
-  | `(tactic| symm $(loc)) => do
+  | `(tactic| symm $(loc?)?) => do
     let atHyp h := liftMetaTactic1 fun g => g.applySymmAt h
     let atTarget := liftMetaTactic1 fun g => g.applySymm
-    withLocation (expandOptLocation loc) atHyp atTarget fun _ => throwError "symm made no progress"
+    let loc := if let some loc := loc? then expandLocation loc else Location.targets #[] true
+    withLocation loc atHyp atTarget fun _ => throwError "symm made no progress"
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.symmSaturate]
diff --git a/src/Lean/LabelAttribute.lean b/src/Lean/LabelAttribute.lean
index c7b49690eea8..f6f16f9584e9 100644
--- a/src/Lean/LabelAttribute.lean
+++ b/src/Lean/LabelAttribute.lean
@@ -72,6 +72,20 @@ def registerLabelAttr (attrName : Name) (attrDescr : String)
   labelExtensionMapRef.modify fun map => map.insert attrName ext
   return ext
 
+/--
+Initialize a new "label" attribute.
+Declarations tagged with the attribute can be retrieved using `Std.Tactic.LabelAttr.labelled`.
+-/
+macro (name := _root_.Lean.Parser.Command.registerLabelAttr)
+  doc:(docComment)? "register_label_attr " id:ident : command => do
+  let str := id.getId.toString
+  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
+  let descr := quote (removeLeadingSpaces
+    (doc.map (·.getDocString) |>.getD ("labelled declarations for " ++ id.getId.toString)))
+  `($[$doc:docComment]? initialize ext : Lean.LabelExtension ←
+      registerLabelAttr $(quote id.getId) $descr $(quote id.getId)
+    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str : attr)
+
 /-- When `attrName` is an attribute created using `register_labelled_attr`,
 return the names of all declarations labelled using that attribute. -/
 def labelled (attrName : Name) : CoreM (Array Name) := do