add changelog

Villetaneuse · May 27, 2024 · 4b85ccc · 4b85ccc
1 parent ac41940
commit 4b85ccc
Showing 1 changed file with 9 additions and 0 deletions.
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
@@ -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).