aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/10-standard-library/12014-ollibs-vector.rst10
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).