chore: Add changelog entry

TDiazT · TDiazT · commit 604730b77835 · 2026-01-10T12:33:24.000+01:00
diff --git a/doc/changelog/01-kernel/21453-remove-type-to-sorts-Changed.rst b/doc/changelog/01-kernel/21453-remove-type-to-sorts-Changed.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  `Type` does not eliminate to any sort by default
+  (`#21453 <https://github.com/rocq-prover/rocq/pull/21453>`_,
+  by Tomas Diaz).
