aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/10-standard-library
diff options
context:
space:
mode:
authorOlivier Laurent2020-12-28 19:14:13 +0100
committerOlivier Laurent2021-03-16 21:06:41 +0100
commite38f64e024c94ad188e186506356980534ab604b (patch)
tree493f6290e8fa80785bdb0998d377ee687c9671d1 /doc/changelog/10-standard-library
parent36a54c1d891c6d853a218e66f9ce8f011311c855 (diff)
correct changelog #13582
Diffstat (limited to 'doc/changelog/10-standard-library')
-rw-r--r--doc/changelog/10-standard-library/13582-exp_ineq.rst4
1 files changed, 1 insertions, 3 deletions
diff --git a/doc/changelog/10-standard-library/13582-exp_ineq.rst b/doc/changelog/10-standard-library/13582-exp_ineq.rst
index 27d89b2f8b..ff4e8db8b0 100644
--- a/doc/changelog/10-standard-library/13582-exp_ineq.rst
+++ b/doc/changelog/10-standard-library/13582-exp_ineq.rst
@@ -4,6 +4,4 @@
Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <).
(`#13582 <https://github.com/coq/coq/pull/13582>`_,
- by Avi Shinnar and Barry Trager, with help from Laurent Théry
-
-).
+ by Avi Shinnar and Barry Trager, with help from Laurent Théry).