fix: register namespaces for types under the module system (#13981)

This PR fixes a private inductive type not being usable as a namespace
immediately after its definition.

Fixes #13929

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: Kha

src/Lean/AddDecl.lean

@@ -50,6 +50,8 @@ private def isNamespaceName : Name → Bool
   | _                 => false
 
 private def registerNamePrefixes (env : Environment) (name : Name) : Environment :=
+  -- namespaces are based on the un-encoded name (`isNamespaceName` is false for any private name)
+  let name := privateToUserName name
   match name with
     | .str _ s =>
       if s.front == '_' then

tests/elab/13929.lean

@@ -0,0 +1,18 @@
+module
+
+/-! Private inductives should also generate open-able namespaces. -/
+
+inductive T where
+  | a
+  | b
+
+structure S where
+  c : Unit
+  d : Nat
+
+open T
+open S
+
+def t1 : T := a
+def t2 : T := b
+def useProj (s : S) : Nat := s.d