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 /plugins/syntax/string_notation.mli | |
| parent | ae5f5ba7f7e673dfeb06a9feaa4271fc165d01f3 (diff) | |
| parent | 5169633a26d2639ec43b4ec82dff11348e380825 (diff) | |
Merge PR #12716: deprecate prod_curry and prod_uncurry
Reviewed-by: anton-trunov
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions