diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 5a6b1fb991..4d7271f580 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -722,6 +722,8 @@ opaque elabEval : CommandElab
   match stx with
   | `($doc:docComment add_decl_doc $id) =>
     let declName ← resolveGlobalConstNoOverloadWithInfo id
+    unless ((← getEnv).getModuleIdxFor? declName).isNone do
+      throwError "invalid 'add_decl_doc', declaration is in an imported module"
     if let .none ← findDeclarationRangesCore? declName then
       -- this is only relevant for declarations added without a declaration range
       -- in particular `Quot.mk` et al which are added by `init_quot`
diff --git a/tests/lean/docStr.lean b/tests/lean/docStr.lean
index 44f710a63e..61d7ad2629 100644
--- a/tests/lean/docStr.lean
+++ b/tests/lean/docStr.lean
@@ -102,3 +102,6 @@ def printRangesTest : MetaM Unit := do
   printRanges `g.foo
 
 #eval printRangesTest
+
+/-- no dice -/
+add_decl_doc Nat.add
diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out
index c6094eae6f..64dd47866b 100644
--- a/tests/lean/docStr.lean.expected.out
+++ b/tests/lean/docStr.lean.expected.out
@@ -189,3 +189,4 @@ g.foo :=
                         charUtf16 := 44,
                         endPos := { line := 42, column := 47 },
                         endCharUtf16 := 47 } }
+docStr.lean:106:0-107:20: error: invalid 'add_decl_doc', declaration is in an imported module