From 869e42b7c3f8ae96cfcd384dc9396aaccc61ada1 Mon Sep 17 00:00:00 2001
From: thorimur <68410468+thorimur@users.noreply.github.com>
Date: Thu, 29 Aug 2024 11:57:14 -0400
Subject: [PATCH] fix: handle `AttributeKind`s in `LabelAttribute`s correctly
 (#3698)

This PR propagates the `AttributeKind` to `SimpleScopedEnvExtension.add`
in attributes created with `register_label_attr`.

This also fixes a nearby stale docstring which referenced `Std`.

---

Closes #3697
---
 src/Lean/LabelAttribute.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/LabelAttribute.lean b/src/Lean/LabelAttribute.lean
index e9db573f8cdc..97daaf6484b7 100644
--- a/src/Lean/LabelAttribute.lean
+++ b/src/Lean/LabelAttribute.lean
@@ -52,8 +52,8 @@ registerBuiltinAttribute {
   name  := attrName
   descr := attrDescr
   applicationTime := AttributeApplicationTime.afterCompilation
-  add   := fun declName _ _ =>
-    ext.add declName
+  add   := fun declName _ kind =>
+    ext.add declName kind
   erase := fun declName => do
     let s := ext.getState (← getEnv)
     modifyEnv fun env => ext.modifyState env fun _ => s.erase declName
@@ -74,7 +74,7 @@ def registerLabelAttr (attrName : Name) (attrDescr : String)
 
 /--
 Initialize a new "label" attribute.
-Declarations tagged with the attribute can be retrieved using `Std.Tactic.LabelAttr.labelled`.
+Declarations tagged with the attribute can be retrieved using `Lean.labelled`.
 -/
 macro (name := _root_.Lean.Parser.Command.registerLabelAttr)
   doc:(docComment)? "register_label_attr " id:ident : command => do