aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/changelog/10-standard-library/09379-splitAt.rst7
1 files changed, 4 insertions, 3 deletions
diff --git a/doc/changelog/10-standard-library/09379-splitAt.rst b/doc/changelog/10-standard-library/09379-splitAt.rst
index af00213c9c..1e6ccb2eaa 100644
--- a/doc/changelog/10-standard-library/09379-splitAt.rst
+++ b/doc/changelog/10-standard-library/09379-splitAt.rst
@@ -1,4 +1,5 @@
-- Added ``uncons`` and ``splitAt`` functions over vectors,
- and proved some lemmas about them
+- Added ``splitAt`` function and lemmas about ``splitAt`` and ``uncons``
(`#9379 <https://github.com/coq/coq/pull/9379>`_,
- by Yishuai Li, with help of Konstantinos Kallas).
+ by Yishuai Li, with help of Konstantinos Kallas,
+ follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_,
+ which added ``uncons`` in 8.10+beta1).