Changelog for 8.17.1.

Zimmi48 · Jun 22, 2023 · 5b4391e · 5b4391e
1 parent 312f93f
commit 5b4391e
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 12 deletions.
diff --git a/doc/changelog/13-misc/17324-master+fix14843-extraction-collision-record-field.rst b/doc/changelog/13-misc/17324-master+fix14843-extraction-collision-record-field.rst
diff --git a/doc/changelog/13-misc/17495-byextendmsg.rst b/doc/changelog/13-misc/17495-byextendmsg.rst
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
@@ -679,6 +679,33 @@ Miscellaneous
   (`#16725 <https://github.com/coq/coq/pull/16725>`_,
   by Jim Fehrle).
 
+Changes in 8.17.1
+~~~~~~~~~~~~~~~~~
+
+A variety of bug fixes and improvements to error messages, including:
+
+- **Fixed:**
+  coqdep generating wrong dependencies when looking for META files
+  (`#17270 <https://github.com/coq/coq/pull/17270>`_,
+  fixes `#16571 <https://github.com/coq/coq/issues/16571>`_,
+  by Rodolphe Lepigre).
+- **Fixed:**
+  Shadowing of record fields in extraction to OCaml
+  (`#17324 <https://github.com/coq/coq/pull/17324>`_,
+  fixes `#12813 <https://github.com/coq/coq/issues/12813>`_
+  and `#14843 <https://github.com/coq/coq/issues/14843>`_
+  and `#16677 <https://github.com/coq/coq/issues/16677>`_,
+  by Hugo Herbelin).
+- **Fixed:**
+  an impossible to turn off debug message "backtracking and redoing byextend on ..."
+  (`#17495 <https://github.com/coq/coq/pull/17495>`_,
+  fixes `#17488 <https://github.com/coq/coq/issues/17488>`_,
+  by Gaëtan Gilbert).
+- **Fixed:**
+  major memory regression affecting MathComp 2
+  (`#17743 <https://github.com/coq/coq/pull/17743>`_,
+  by Enrico Tassi).
+
 Version 8.16
 ------------