diff options
Diffstat (limited to 'doc')
4 files changed, 21 insertions, 0 deletions
diff --git a/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst b/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst new file mode 100644 index 0000000000..1bf62de3fd --- /dev/null +++ b/doc/changelog/01-kernel/12738-fix-sr-cumul-inds.rst @@ -0,0 +1,5 @@ +- **Fixed:** Incompleteness of conversion checking on problems + involving :ref:`eta-expansion` and :ref:`cumulative universe + polymorphic inductive types <cumulative>` (`#12738 + <https://github.com/coq/coq/pull/12738>`_, fixes `#7015 + <https://github.com/coq/coq/issues/7015>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst b/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst new file mode 100644 index 0000000000..289d17167d --- /dev/null +++ b/doc/changelog/04-tactics/12816-master+fix12787-K-redex-injection-anomaly.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Anomaly with :tacn:`injection` involving artificial + dependencies disappearing by reduction + (`#12816 <https://github.com/coq/coq/pull/12816>`_, + fixes `#12787 <https://github.com/coq/coq/issues/12787>`_, + by Hugo Herbelin). diff --git a/doc/changelog/10-standard-library/12801-cyclic-set.rst b/doc/changelog/10-standard-library/12801-cyclic-set.rst new file mode 100644 index 0000000000..9a07d78144 --- /dev/null +++ b/doc/changelog/10-standard-library/12801-cyclic-set.rst @@ -0,0 +1,5 @@ +- **Changed:** + Change the sort of cyclic numbers from Type to Set. For backward compatibility, a dynamic sort was defined in the 3 packages bignums, coqprime and color. + See for example commit 6f62bda in bignums. + (`#12801 <https://github.com/coq/coq/pull/12801>`_, + by Vincent Semeria). diff --git a/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst b/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst new file mode 100644 index 0000000000..c754826e62 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst @@ -0,0 +1,5 @@ +- **Fixed:** + ``make approve-output`` in the test-suite now correctly handles + ``output-coqtop`` and ``output-coqchk`` tests (`#12864 + <https://github.com/coq/coq/pull/12864>`_, fixes `#12863 + <https://github.com/coq/coq/issues/12863>`_, by Jason Gross). |