aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYishuai Li2019-06-29 14:05:28 -0400
committerYishuai Li2019-09-01 02:10:02 -0400
commit7ee359556287610fde675f936f74ab3ab37d8e00 (patch)
treecee6716267db4f5d876a4fc441cea166b2a2dd8d
parentea23c93e33131216cff049a908a3e423dc704624 (diff)
Changelog: more accurate on uncons
-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).