docs: describe EXTERN redeclaration and verified lli runs

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

3 files changed, 6 insertions, 3 deletions

diff --git a/AGENTS/PITFALLS.md b/AGENTS/PITFALLS.md
index 551a64c..e7047cf 100644
--- a/AGENTS/PITFALLS.md
+++ b/AGENTS/PITFALLS.md
@@ -151,7 +151,8 @@ test programs.
   The driver checks every EXTERN symbol against INCLUDE_OBJ inputs before CodeGen;
   `"__libc"` must be included explicitly even though the runtime always links libc.
   Only `.o` user objects; INCLUDE_OBJ is global across inputs. `-S` does not link them.
-  Two EXTERNs differing only in case conflict (pseudocode names are case insensitive).
+  Identical EXTERN redeclarations (same or other files, CIdentity-equal types) are allowed;
+  differing ones fail. Two EXTERNs differing only in case conflict (pseudocode names are case insensitive).
 
 ## Not implemented (9618 features)
 
diff --git a/AGENTS/SUBSYSTEMS.md b/AGENTS/SUBSYSTEMS.md
index 866d39e..5a57340 100644
--- a/AGENTS/SUBSYSTEMS.md
+++ b/AGENTS/SUBSYSTEMS.md
@@ -47,6 +47,8 @@ ArrayTable) afterwards.
 `PrototypeAST` (IsExternal, IsVariadic, unnamed `argN` params). `FunctionGen::emitExternPrototype`
 validates C types, records a `FuncSig` with `IsExternal`, the declared `FunctionType` and
 sext/zext attributes for sub-32-bit integers, and `getOrInsertFunction`s the exact symbol.
+Identical redeclarations append a FuncSig per declaring unit (visibility unchanged) and
+`resolveCall` takes the first visible one; mismatched signatures are errors.
 Calls go through `FunctionGen::emitCall(const FuncSig &, ...)` with that type, so a
 runtime declaration of the same libc symbol with another type is harmless.
 `CodeGen::emitVariadicArgument` applies C default promotions. The driver (`main.cc`)
@@ -54,7 +56,7 @@ resolves INCLUDE_OBJ paths, reads defined global symbols with `llvm::object`
 (`collectObjectSymbols`; `"__libc"` uses `collectLibcSymbols` over the embedded runtime's
 libc/libm inputs, copied to aligned buffers), rejects missing symbols, and passes objects
 to `compileNative`, `runEmbedded` (`addObjectFile`) or lli (`-extra-object=`).
-Linux is verified; the Windows/macOS libc file-name rules and the lli path are not.
+Linux EMBEDDED and PATH (lli) runs are verified; the Windows/macOS libc file-name rules are not.
 
 **User types** (`TypeSystem` + `Designator.cc` + `TypeCheckGen.cc`):
 `Designator.cc` owns the type pre-pass and lvalue access; `TypeCheckGen.cc` owns
diff --git a/doc/language/keyword/cpsc-keyword-extern.7.md b/doc/language/keyword/cpsc-keyword-extern.7.md
index db1bde4..5797a4f 100644
--- a/doc/language/keyword/cpsc-keyword-extern.7.md
+++ b/doc/language/keyword/cpsc-keyword-extern.7.md
@@ -19,7 +19,7 @@ Parameters list only types. Parameter and result types must be C types: C_INT, C
 
 A final `...` makes the function variadic. Variadic arguments must also be C values; they receive C default argument promotions (float to double, narrow integers and _Bool to int or unsigned int).
 
-Every EXTERN symbol must be defined by an object named with INCLUDE_OBJ, otherwise compilation fails. EXTERN cannot be combined with OVERLOAD, and a name may be declared once across all input files; put shared declarations in one file and INCLUDE it.
+Every EXTERN symbol must be defined by an object named with INCLUDE_OBJ, otherwise compilation fails. EXTERN cannot be combined with OVERLOAD or share a name with a FUNCTION or PROCEDURE. As in C, the same function may be declared again in the same or another input file when the signature is identical (equivalent C aliases match); conflicting declarations are errors. Each file sees its own declarations and those of the files it includes.
 
 # EXAMPLE