11 files changed, 36 insertions, 21 deletions
diff --git a/doc/changelog/03-notations/13842-remove-decimal.rst b/doc/changelog/03-notations/13842-remove-decimal.rst
new file mode 100644
index 0000000000..4bc26ef6a8
--- /dev/null
+++ b/doc/changelog/03-notations/13842-remove-decimal.rst
@@ -0,0 +1,3 @@
+- **Removed:**
+  Remove decimal-only number notations which were deprecated in 8.12.
+  (`#13842 <https://github.com/coq/coq/pull/13842>`_, by Pierre Roux).
diff --git a/doc/changelog/11-infrastructure-and-dependencies/12567-dune+split_stdlib.rst b/doc/changelog/11-infrastructure-and-dependencies/12567-dune+split_stdlib.rst
new file mode 100644
index 0000000000..6fe6f62faa
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/12567-dune+split_stdlib.rst
@@ -0,0 +1,14 @@
+- **Changed:**
+  Coq's configure script now requires absolute paths for the `-prefix`
+  option.
+  (`#12567 <https://github.com/coq/coq/pull/12567>`_,
+  by Emilio Jesus Gallego Arias).
+
+- **Changed:**
+  The regular Coq package has been split in two: coq-core, with
+  OCaml-based libraries and tools; and coq-stdlib, which contains the
+  Gallina-based standard library. The package Coq now depends on both
+  for compatiblity.
+  (`#12567 <https://github.com/coq/coq/pull/12567>`_,
+  by Emilio Jesus Gallego Arias, review by Vincent Laporte, Guillaume
+  Melquiond, Enrico Tassi, and Théo Zimmerman).
diff --git a/doc/dune b/doc/dune
index c82e5a3df4..97bd437097 100644
--- a/doc/dune
+++ b/doc/dune
@@ -13,7 +13,8 @@
   ;   + %{bin:coqdoc} etc...
   ;   + config/coq_config.py
   ;   + tools/coqdoc/coqdoc.css
-  (package coq)
+  (package coq-core)
+  (package coq-stdlib)
   (source_tree sphinx)
   (source_tree tools/coqrst)
   unreleased.rst
@@ -26,7 +27,8 @@
  ; Cannot use this deps alias because of ocaml/dune#3415
  ; (deps (alias refman-deps))
  (deps
-  (package coq)
+  (package coq-core)
+  (package coq-stdlib)
   (source_tree sphinx)
   (source_tree tools/coqrst)
   unreleased.rst
@@ -41,7 +43,8 @@
  ; Cannot use this deps alias because of ocaml/dune#3415
  ; (deps (alias refman-deps))
  (deps
-  (package coq)
+  (package coq-core)
+  (package coq-stdlib)
   (source_tree sphinx)
   (source_tree tools/coqrst)
   unreleased.rst
diff --git a/doc/plugin_tutorial/tuto0/src/dune b/doc/plugin_tutorial/tuto0/src/dune
index ab9b4dd531..c7ed997221 100644
--- a/doc/plugin_tutorial/tuto0/src/dune
+++ b/doc/plugin_tutorial/tuto0/src/dune
@@ -1,6 +1,6 @@
 (library
  (name tuto0_plugin)
- (public_name coq.plugins.tutorial.p0)
- (libraries coq.plugins.ltac))
+ (public_name coq-core.plugins.tutorial.p0)
+ (libraries coq-core.plugins.ltac))
 
 (coq.pp (modules g_tuto0))
diff --git a/doc/plugin_tutorial/tuto1/src/dune b/doc/plugin_tutorial/tuto1/src/dune
index 054d5ecd26..bf87222e16 100644
--- a/doc/plugin_tutorial/tuto1/src/dune
+++ b/doc/plugin_tutorial/tuto1/src/dune
@@ -1,6 +1,6 @@
 (library
  (name tuto1_plugin)
- (public_name coq.plugins.tutorial.p1)
- (libraries coq.plugins.ltac))
+ (public_name coq-core.plugins.tutorial.p1)
+ (libraries coq-core.plugins.ltac))
 
 (coq.pp (modules g_tuto1))
diff --git a/doc/plugin_tutorial/tuto2/src/dune b/doc/plugin_tutorial/tuto2/src/dune
index 8c4b04b1ae..0797debccf 100644
--- a/doc/plugin_tutorial/tuto2/src/dune
+++ b/doc/plugin_tutorial/tuto2/src/dune
@@ -1,6 +1,6 @@
 (library
  (name tuto2_plugin)
- (public_name coq.plugins.tutorial.p2)
- (libraries coq.plugins.ltac))
+ (public_name coq-core.plugins.tutorial.p2)
+ (libraries coq-core.plugins.ltac))
 
 (coq.pp (modules g_tuto2))
diff --git a/doc/plugin_tutorial/tuto3/src/dune b/doc/plugin_tutorial/tuto3/src/dune
index 678dd71328..dcecf0852e 100644
--- a/doc/plugin_tutorial/tuto3/src/dune
+++ b/doc/plugin_tutorial/tuto3/src/dune
@@ -1,7 +1,7 @@
 (library
  (name tuto3_plugin)
- (public_name coq.plugins.tutorial.p3)
+ (public_name coq-core.plugins.tutorial.p3)
  (flags :standard -warn-error -3)
- (libraries coq.plugins.ltac))
+ (libraries coq-core.plugins.ltac))
 
 (coq.pp (modules g_tuto3))
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index ea099eb52e..8fa1b97851 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -82,13 +82,13 @@ Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack,
 Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia
 and Théo Zimmermann.
 
-The 52 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric
+The 51 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric
 Besson, Lasse Blaauwbroek, Clément Blaudeau, Martin Bodin, Ali Caglayan, Tej Chajed,
 Cyril Cohen, Julien Coolen, Matthew Dempsky, Maxime Dénès, Andres Erbsen,
 Jim Fehrle, Emilio Jesús Gallego Arias, Paolo G. Giarrusso, Attila Gáspár, Gaëtan Gilbert,
 Jason Gross, Benjamin Grégoire, Hugo Herbelin, Wolf Honore, Jasper Hugunin, Ignat Insarov,
 Ralf Jung, Fabian Kunze, Vincent Laporte, Olivier Laurent, Larry D. Lee Jr,
-Thomas Letan, Yishuai Li, Xia Li-yao, James Lottes, Jean-Christophe Léchenet,
+Thomas Letan, Yishuai Li, James Lottes, Jean-Christophe Léchenet,
 Kenji Maillard, Erik Martin-Dorel, Yusuke Matsushita, Guillaume Melquiond,
 Carl Patenaude-Poulin, Clément Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux,
 Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Matthieu Sozeau,
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 03571ad680..557ef10555 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1726,12 +1726,6 @@ Number notations
             * :n:`@qualid__type -> Number.number`
             * :n:`@qualid__type -> option Number.number`
 
-         .. deprecated:: 8.12
-            Number notations on :g:`Decimal.uint`, :g:`Decimal.int` and
-            :g:`Decimal.decimal` are replaced respectively by number
-            notations on :g:`Number.uint`, :g:`Number.int` and
-            :g:`Number.number`.
-
          When parsing, the application of the parsing function
          :n:`@qualid__parse` to the number will be fully reduced, and universes
          of the resulting term will be refreshed.
diff --git a/doc/stdlib/dune b/doc/stdlib/dune
index 0b6ca5f178..6b51202f6e 100644
--- a/doc/stdlib/dune
+++ b/doc/stdlib/dune
@@ -22,7 +22,8 @@
    (:header %{project_root}/doc/common/styles/html/coqremote/header.html)
    (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html)
    ; For .glob files, should be gone when Coq Dune is smarter.
-   (package coq))
+   (package coq-core)
+   (package coq-stdlib))
  (action
   (progn
    (run mkdir -p html)
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index 1c07d00d4f..4ba60ddd9f 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -1,6 +1,6 @@
 (executable
  (name doc_grammar)
- (libraries coq.clib coqpp))
+ (libraries coq-core.clib coqpp))
 
 (env (_ (binaries doc_grammar.exe)))