diff --git a/src/Lean/Elab/InheritDoc.lean b/src/Lean/Elab/InheritDoc.lean index a4d3464671..b629a9e124 100644 --- a/src/Lean/Elab/InheritDoc.lean +++ b/src/Lean/Elab/InheritDoc.lean @@ -16,12 +16,12 @@ builtin_initialize unless kind == AttributeKind.global do throwError "invalid `[inherit_doc]` attribute, must be global" match stx with - | `(attr| inherit_doc $[$id?:ident]?) => + | `(attr| inherit_doc $[$id?:ident]?) => withRef stx[0] do let some id := id? | throwError "invalid `[inherit_doc]` attribute, could not infer doc source" let declName ← Elab.resolveGlobalConstNoOverloadWithInfo id if (← findDocString? (← getEnv) decl).isSome then - logWarningAt id m!"{← mkConstWithLevelParams decl} already has a doc string" + logWarning m!"{← mkConstWithLevelParams decl} already has a doc string" let some doc ← findDocString? (← getEnv) declName | logWarningAt id m!"{← mkConstWithLevelParams declName} does not have a doc string" addDocString decl doc