Merge PR coq#18530: Integrate last changelogs for 8.19

Reviewed-by: proux01 Co-authored-by: proux01 <[email protected]>
SkySkimmer · Jan 22, 2024 · 8561d71 · 8561d71
2 parents d7f9d03 + 1ee5fa0
commit 8561d71
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 11 deletions.
diff --git a/doc/changelog/01-kernel/18507-fix-subtype-prim.rst b/doc/changelog/01-kernel/18507-fix-subtype-prim.rst
diff --git a/doc/changelog/09-cli-tools/18448-master+fix18434-coqdoc-external-regression.rst b/doc/changelog/09-cli-tools/18448-master+fix18434-coqdoc-external-regression.rst
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
@@ -138,6 +138,11 @@ Kernel
   (`#17836 <https://github.com/coq/coq/pull/17836>`_,
   `#18331 <https://github.com/coq/coq/pull/18331>`_,
   by Gaëtan Gilbert).
+- **Fixed:**
+  Primitives being incorrectly considered convertible to anything by module subtyping
+  (`#18507 <https://github.com/coq/coq/pull/18507>`_,
+  fixes `#18503 <https://github.com/coq/coq/issues/18503>`_,
+  by Gaëtan Gilbert).
 
 Specification language, type inference
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -550,6 +555,12 @@ Command-line tools
   Spurious `coqdep` warnings due to missing path normalization for plugins
   (`#18165 <https://github.com/coq/coq/pull/18165>`_,
   by Rodolphe Lepigre).
+- **Fixed:**
+  Regression in option :g:`--external` of `coqdoc`, whose two arguments
+  were inadvertently swapped
+  (`#18448 <https://github.com/coq/coq/pull/18448>`_,
+  fixes `#18434 <https://github.com/coq/coq/issues/18434>`_,
+  by Hugo Herbelin).
 
 .. _819Stdlib: