From 22cdac914d74caafd7acffef9940d0d6609fcef5 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 7 Nov 2022 21:11:41 +0100 Subject: [PATCH] fix: improved error span for `inherit_doc` (#1807) --- src/Lean/Elab/InheritDoc.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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