Merge PR #21653: [refman] Renaming Stdlib -> Corelib

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

Author: coqbot-app[bot]

doc/sphinx/addendum/universe-polymorphism.rst

@@ -612,7 +612,7 @@ Printing universes
    names (adjusting constraints to preserve the implied transitive
    constraints between kept universes). :n:`@debug_univ_name` is
    :n:`@qualid` for named universes (e.g. `eq.u0`), and :n:`@string`
-   for raw universe expressions (e.g. `"Stdlib.Init.Logic.1"`).
+   for raw universe expressions (e.g. `"Corelib.Init.Logic.1"`).
 
    By default when printing a subgraph `Print Universes` attempts to
    find and print the source of the constraints. This can be

doc/sphinx/language/core/assumptions.rst

@@ -38,7 +38,7 @@ variable can be introduced at the same time. It is also possible to give
 the type of the variable as follows:
 :n:`(@ident : @type := @term)`.
 
-`(x : T | P)` is syntactic sugar for `(x : @Stdlib.Init.Specif.sig _ (fun x : T => P))`,
+`(x : T | P)` is syntactic sugar for `(x : @Corelib.Init.Specif.sig _ (fun x : T => P))`,
 which would more typically be written `(x : {x : T | P})`.
 Since `(x : T | P)` uses `sig` directly,
 changing the notation `{x : T | P}`

doc/sphinx/language/core/modules.rst

@@ -360,11 +360,11 @@ are now available through the dot notation.
 .. cmd:: Print Namespace @dirpath
 
    Prints the names and types of all loaded constants whose fully qualified
-   names start with :n:`@dirpath`. For example, the command ``Print Namespace Stdlib.``
-   displays the names and types of all loaded constants in the standard library.
-   The command ``Print Namespace Stdlib.Init`` only shows constants defined in one
+   names start with :n:`@dirpath`. For example, the command ``Print Namespace Corelib.``
+   displays the names and types of all loaded constants in the core library.
+   The command ``Print Namespace Corelib.Init`` only shows constants defined in one
    of the files in the ``Init`` directory. The command ``Print Namespace
-   Stdlib.Init.Nat`` shows what is in the ``Nat`` library file inside the ``Init``
+   Corelib.Init.Nat`` shows what is in the ``Nat`` library file inside the ``Init``
    directory. Module names may appear in :n:`@dirpath`.
 
    .. example::
@@ -562,7 +562,7 @@ While qualified names always consist of a series of dot-separated :n:`@ident`\s,
 
 **File part.** Files are identified by :gdef:`logical paths <logical path>`,
 which are prefixes in the form :n:`{* @ident__logical } {+ @ident__file }`, such
-as :n:`Stdlib.Init.Logic`, in which:
+as :n:`Corelib.Init.Logic`, in which:
 
 - :n:`{* @ident__logical }`, the :gdef:`logical name`, maps to one or more
   directories (or :gdef:`physical paths <physical path>`) in the user's file system.
@@ -587,14 +587,14 @@ with the logical name :n:`Top` and there is no associated file system path.
 
 - :n:`@ident__base` is the base name used in the command defining
   the item.  For example, :n:`eq` in the :cmd:`Inductive` command defining it
-  in `Stdlib.Init.Logic` is the base name for `Stdlib.Init.Logic.eq`, the standard library
+  in `Corelib.Init.Logic` is the base name for `Corelib.Init.Logic.eq`, the core library
   definition of :term:`Leibniz equality`.
 
 If :n:`@qualid` is the fully qualified name of an item, Rocq
 always interprets :n:`@qualid` as a reference to that item.  If :n:`@qualid` is also a
 partially qualified name for another item, then you must provide a more-qualified
 name to uniquely identify that other item.  For example, if there are two
-fully qualified items named `Foo.Bar` and `Stdlib.X.Foo.Bar`, then `Foo.Bar` refers
+fully qualified items named `Foo.Bar` and `Corelib.X.Foo.Bar`, then `Foo.Bar` refers
 to the first item and `X.Foo.Bar` is the shortest name for referring to the second item.
 
 Definitions with the :attr:`local` attribute are only accessible with

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -519,7 +519,7 @@ Requests to the environment
       Locate nat.
       Locate Datatypes.O.
       Locate Init.Datatypes.O.
-      Locate Stdlib.Init.Datatypes.O.
+      Locate Corelib.Init.Datatypes.O.
       Locate I.Dont.Exist.
 
 .. _printing-flags:
@@ -605,7 +605,7 @@ file is a particular case of a module called a *library file*.
    (if :n:`From @dirpath` is given) or :n:`{* @ident__implicit. }@qualid` (if
    the optional `From` clause is absent). :n:`{* @ident__implicit. }` represents
    the parts of the fully qualified name that are implicit.  For example,
-   `From Stdlib Require Nat` loads `Stdlib.Init.Nat` and `Init` is implicit.
+   `From Corelib Require Nat` loads `Corelib.Init.Nat` and `Init` is implicit.
    :n:`@ident` is the final component of the :n:`@qualid`.
 
    If a file is found, its logical name must be the same as the one