Adding changelog for coq#17889

herbelin · Jul 26, 2023 · 4d3970f · 4d3970f
1 parent fc76ccb
commit 4d3970f
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/...13-misc/17889-master+fix17817-extraction-prop-elim-error-not-ocaml-specific.rst b/...13-misc/17889-master+fix17817-extraction-prop-elim-error-not-ocaml-specific.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Refer to the correct chosen extraction language in the
+  sort-polymorphic singleton inductive type extraction error message
+  (`#17889 <https://github.com/coq/coq/pull/17889>`_,
+  fixes `#17817 <https://github.com/coq/coq/issues/17817>`_,
+  by Hugo Herbelin).