add properties of operations on vectors

1 files changed, 10 insertions, 0 deletions

diff --git a/doc/changelog/10-standard-library/12014-ollibs-vector.rst b/doc/changelog/10-standard-library/12014-ollibs-vector.rst
new file mode 100644
index 0000000000..87625dd23b
--- /dev/null
+++ b/doc/changelog/10-standard-library/12014-ollibs-vector.rst
@@ -0,0 +1,10 @@
+- **Added:**
+  Properties of some operations on vectors:
+
+  - ``nth_order``: ``nth_order_hd``, ``nth_order_tl``, ``nth_order_ext``
+  - ``replace``: ``nth_order_replace_eq``, ``nth_order_replace_neq``, ``replace_id``, ``replace_replace_eq``, ``replace_replace_neq``
+  - ``map``: ``map_id``, ``map_map``, ``map_ext_in``, ``map_ext``
+  - ``Forall`` and ``Forall2``: ``Forall_impl``, ``Forall_forall``, ``Forall_nth_order``, ``Forall2_nth_order``
+
+  (`#12014 <https://github.com/coq/coq/pull/12014>`_,
+  by Olivier Laurent).