From 05cf2d04aee51c67e67abbaf432e038251809e3a Mon Sep 17 00:00:00 2001
From: ilya
Date: Sat, 11 Apr 2020 13:59:48 +0300
Subject: 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
---
 doc/changelog/10-standard-library/12044-issue-12015.rst | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 doc/changelog/10-standard-library/12044-issue-12015.rst

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)).
-- 
cgit v1.2.3