From 4b85ccc4bf2ba787d0baff1453701f9c9ae1e2f1 Mon Sep 17 00:00:00 2001
From: Pierre Rousselin <rousselin@math.univ-paris13.fr>
Date: Mon, 27 May 2024 13:41:13 +0200
Subject: [PATCH] add changelog

---
 .../18482-remove-include-type.rst                        | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 doc/changelog/08-vernac-commands-and-options/18482-remove-include-type.rst

diff --git a/doc/changelog/08-vernac-commands-and-options/18482-remove-include-type.rst b/doc/changelog/08-vernac-commands-and-options/18482-remove-include-type.rst
new file mode 100644
index 000000000000..fe5b5c178b82
--- /dev/null
+++ b/doc/changelog/08-vernac-commands-and-options/18482-remove-include-type.rst
@@ -0,0 +1,9 @@
+- **Removed:**
+  the `Include Type` command after a long period of deprecation
+  (`#18482 <https://github.com/coq/coq/pull/18482>`_,
+  by Pierre Rousselin).
+- **Changed:**
+  The `Include` command can now include module types with a `with` declaration
+  to instantiate some parameters
+  (`#18482 <https://github.com/coq/coq/pull/18482>`_,
+  by Pierre Rousselin).