diff options
| author | Anton Trunov | 2020-08-13 18:27:34 +0300 |
|---|---|---|
| committer | Anton Trunov | 2020-08-13 18:27:34 +0300 |
| commit | 226ed2069d9874fe845a1995053783f811ace9ae (patch) | |
| tree | 364c569bbce80a00482758109a4548eb7daa782c /doc | |
| parent | ae5f5ba7f7e673dfeb06a9feaa4271fc165d01f3 (diff) | |
| parent | 5169633a26d2639ec43b4ec82dff11348e380825 (diff) | |
Merge PR #12716: deprecate prod_curry and prod_uncurry
Reviewed-by: anton-trunov
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/12716-curry.rst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/12716-curry.rst b/doc/changelog/10-standard-library/12716-curry.rst new file mode 100644 index 0000000000..51b59e4a94 --- /dev/null +++ b/doc/changelog/10-standard-library/12716-curry.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` + (`#12716 <https://github.com/coq/coq/pull/12716>`_, + by Yishuai Li). |