From fff68a50ebb67c7f7ab0056a0da49cbf3dcdf40c Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sun, 15 Sep 2024 11:34:33 +0200
Subject: [PATCH] Add changelog

---
 .../19310-stdlib-logical-name.rst             | 34 +++++++++++++------
 .../11-standard-library/19530-stdlib_repo.rst |  5 +++
 2 files changed, 28 insertions(+), 11 deletions(-)
 create mode 100644 doc/changelog/11-standard-library/19530-stdlib_repo.rst

diff --git a/doc/changelog/11-standard-library/19310-stdlib-logical-name.rst b/doc/changelog/11-standard-library/19310-stdlib-logical-name.rst
index 94c74bc53b90..9912d25916d0 100644
--- a/doc/changelog/11-standard-library/19310-stdlib-logical-name.rst
+++ b/doc/changelog/11-standard-library/19310-stdlib-logical-name.rst
@@ -1,14 +1,26 @@
 - **Changed:**
   the requirement prefix of the standard library from ``Coq`` to
-  ``Stdlib``. For backward compatibility with older versions of Coq
-  ``Coq`` is immediatly translated to ``Stdlib`` with a warning. It is
-  thus not recommended to name anything ``Coq`` or ``Coq.*``. When
-  droping support for Coq <= 8.20, a simple script such as ``for f in
-  $(find . -name "*.v") ; do sed -i $f -e 's/From Coq Require/From
-  Stdlib Require/;s/Coq[.]\([a-zA-Z]\)/Stdlib[.]\1/g' ; done`` should
-  be enough to adapt your code. Meanwhile, adding the two lines
-  ``-arg -w -arg -deprecated-from-Coq`` and
-  ``-arg -w -arg -deprecated-dirpath-Coq``
-  to your ``_CoqProject`` will silence the warnings
-  (`#19310 <https://github.com/coq/coq/pull/19310>`_,
+  ``Stdlib`` and made it mandatory. As a temporary measure, for
+  backward compatibility with older versions, ``Coq``, or a missing
+  `From Stdlib`, is immediatly translated to ``Stdlib`` with a
+  warning. It is thus not recommended to name anything ``Coq`` or
+  ``Coq.*``.
+  The recommended transition path is to first potentially silence
+  the warnings, adding the lines
+  ``-arg -w -arg -deprecated-from-Coq``,
+  ``-arg -w -arg -deprecated-dirpath-Coq`` and
+  ``-arg -w -arg -deprecated-missing-stdlib``
+  or simply the more generic
+  ``-arg -compat -arg 8.20`` to your ``_CoqProject``.
+  Then, when droping support for Coq <= 8.20, replacing requirement of
+  Stdlib modules by `From Stdlib Require {Import,Export,} <LibraryModules>.`.
+  Beware that the Stdlib still has a handful redundant names, that is
+  for modules `Byte`, you still have to use `From Stdlib.Strings` or
+  `From Stdlib.Init`, for `Tactics` use `From Stdlib.Program` or `From
+  Stdlib.Init`, for `Tauto` use `From Stdlib.micromega` of `From
+  Stdlib.Init` and for `Wf`, use `From Stdlib.Program` or `From
+  Stdlib.Init`
+  (`#19310 <https://github.com/coq/coq/pull/19310>`_
+  and `#19530 <https://github.com/coq/coq/pull/19530>`_,
+  the latter starting to implement `CEP#83 <https://github.com/coq/ceps/pull/83>`_
   by Pierre Roux).
diff --git a/doc/changelog/11-standard-library/19530-stdlib_repo.rst b/doc/changelog/11-standard-library/19530-stdlib_repo.rst
new file mode 100644
index 000000000000..17f30bc7434d
--- /dev/null
+++ b/doc/changelog/11-standard-library/19530-stdlib_repo.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  a new `rocq-core` package for users who don't want to depend on Stdlib
+  (`#19530 <https://github.com/coq/coq/pull/19530>`_,
+  starting to implement `CEP#83 <https://github.com/coq/ceps/pull/83>`_
+  by Pierre Roux).