diff options
| author | ilya | 2020-04-11 13:59:48 +0300 |
|---|---|---|
| committer | Jason Gross | 2020-04-19 18:29:55 -0400 |
| commit | 05cf2d04aee51c67e67abbaf432e038251809e3a (patch) | |
| tree | fa7e7d42619404fa238ba754e9320ad190f1ae60 /doc | |
| parent | 8d3f4fcd162c7dd23619f605d55e9a773c131e0e (diff) | |
added changelog for PR 12044
Update doc/changelog/10-standard-library/12044-issue-12015.rst
Co-Authored-By: Jason Gross <jasongross9@gmail.com>
Apply suggestions from code review
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/12044-issue-12015.rst | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/12044-issue-12015.rst b/doc/changelog/10-standard-library/12044-issue-12015.rst new file mode 100644 index 0000000000..166fc80fb0 --- /dev/null +++ b/doc/changelog/10-standard-library/12044-issue-12015.rst @@ -0,0 +1,10 @@ +- **Fixed:** + Rewrote ``Structures.OrderedTypeEx.String_as_OT.compare`` + to avoid huge proof terms + (Fixes `#12015 <https://github.com/coq/coq/issues/12015>`_, + `#12044 <https://github.com/coq/coq/pull/12044>`_, + by formalize.eth (formalize@protonmail.com)). +- **Added:** + Added ``Structures.OrderedTypeEx.Ascii_as_OT`` + (`#12044 <https://github.com/coq/coq/pull/12044>`_, + by formalize.eth (formalize@protonmail.com)). |