fix: handle AttributeKinds in LabelAttributes 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

@@ -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