Merge PR #12734: [changelog] Latest changes backported to 8.12 branch.

Reviewed-by: Zimmi48

11 files changed, 78 insertions, 51 deletions

diff --git a/doc/changelog/03-notations/12523-term-notation-custom.rst b/doc/changelog/03-notations/12523-term-notation-custom.rst
deleted file mode 100644
index 1a611f3fb1..0000000000
--- a/doc/changelog/03-notations/12523-term-notation-custom.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  Simultaneous definition of terms and notations now support custom entries.
-  Fixes `#11121 <https://github.com/coq/coq/pull/11121>`_.
-  (`#12523 <https://github.com/coq/coq/pull/11523>`_, by Maxime Dénès).
diff --git a/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst b/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst
deleted file mode 100644
index ab8768a079..0000000000
--- a/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  Printing bug with notations for n-ary applications used with applied references.
-  (`#12683 <https://github.com/coq/coq/pull/12683>`_,
-  fixes `#12682 <https://github.com/coq/coq/pull/12682>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/04-tactics/12572-fix-12571.rst b/doc/changelog/04-tactics/12572-fix-12571.rst
deleted file mode 100644
index 98b217e86b..0000000000
--- a/doc/changelog/04-tactics/12572-fix-12571.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Fixed:**
-  typeclasses eauto (and discriminated hint bases) now correctly
-  classify local variables as being unfoldable
-  (`#12572 <https://github.com/coq/coq/pull/12572>`_,
-  fixes `#12571 <https://github.com/coq/coq/issues/12571>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/05-tactic-language/12541-fix12228.rst b/doc/changelog/05-tactic-language/12541-fix12228.rst
deleted file mode 100644
index 286760e008..0000000000
--- a/doc/changelog/05-tactic-language/12541-fix12228.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Fixed:**
-  Excluding occurrences was causing an anomaly in tactics
-  (e.g., :g:`pattern _ at L` where :g:`L` is :g:`-2`).
-  (`#12541 <https://github.com/coq/coq/pull/12541>`_,
-  fixes `#12228 <https://github.com/coq/coq/issues/12228>`_,
-  by Pierre Roux).
diff --git a/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst
deleted file mode 100644
index 555020d319..0000000000
--- a/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  Fix the parsing of multi-parameters Ltac2 types
-  (`#12594 <https://github.com/coq/coq/pull/12594>`_,
-  fixes `#12595 <https://github.com/coq/coq/issues/12595>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst b/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst
deleted file mode 100644
index 4df8e97e34..0000000000
--- a/doc/changelog/06-ssreflect/12708-fix-12707-ssr-ast-closure-size.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  Do not store the full environment inside ssr ast_closure_term
-  (`#12708 <https://github.com/coq/coq/pull/12708>`_,
-  fixes `#12707 <https://github.com/coq/coq/issues/12707>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst
deleted file mode 100644
index c654ddd69d..0000000000
--- a/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  Properly report the mismatched magic number of vo files
-  (`#12677 <https://github.com/coq/coq/pull/12677>`_,
-  fixes `#12513 <https://github.com/coq/coq/issues/12513>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/07-commands-and-options/12678-tweak-hint-constr-warning.rst b/doc/changelog/07-commands-and-options/12678-tweak-hint-constr-warning.rst
deleted file mode 100644
index 9de072060d..0000000000
--- a/doc/changelog/07-commands-and-options/12678-tweak-hint-constr-warning.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Changed:**
-  Arbitrary hints have been undeprecated, and their definition
-  now triggers a standard warning instead
-  (`#12678 <https://github.com/coq/coq/pull/12678>`_,
-  fixes `#11970 <https://github.com/coq/coq/issues/11970>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/09-coqide/12562-coqide-lax-filename.rst b/doc/changelog/09-coqide/12562-coqide-lax-filename.rst
deleted file mode 100644
index ef3160dd99..0000000000
--- a/doc/changelog/09-coqide/12562-coqide-lax-filename.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Fixed:** CoqIDE no longer exits when trying to open a file whose name is not a valid identifier
-  (`#12562 <https://github.com/coq/coq/pull/12562>`_,
-  fixes `#10988 <https://github.com/coq/coq/issues/10988>`_,
-  by Vincent Laporte).
diff --git a/doc/changelog/11-infrastructure-and-dependencies/12583-fix-remake.rst b/doc/changelog/11-infrastructure-and-dependencies/12583-fix-remake.rst
deleted file mode 100644
index d9c8b634d6..0000000000
--- a/doc/changelog/11-infrastructure-and-dependencies/12583-fix-remake.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  Running ``make`` in ``test-suite/`` twice (or more) in a row will no longer
-  rebuild the ``modules/`` tests on subsequent runs, if they have not been
-  modified in the meantime (`#12583 <https://github.com/coq/coq/pull/12583>`_,
-  fixes `#12582 <https://github.com/coq/coq/issues/12582>`_, by Jason Gross).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index d4707a04d8..eb930362f5 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -1126,6 +1126,84 @@ Infrastructure and dependencies
   (`#11245 <https://github.com/coq/coq/pull/11245>`_,
   by Emilio Jesus Gallego Arias).
 
+Changes in 8.12.0
+~~~~~~~~~~~~~~~~~~~~~
+
+.. contents::
+   :local:
+
+**Notations**
+
+- **Added:**
+  Simultaneous definition of terms and notations now support custom entries.
+  Fixes `#11121 <https://github.com/coq/coq/pull/11121>`_.
+  (`#12523 <https://github.com/coq/coq/pull/11523>`_, by Maxime Dénès).
+- **Fixed:**
+  Printing bug with notations for n-ary applications used with applied references.
+  (`#12683 <https://github.com/coq/coq/pull/12683>`_,
+  fixes `#12682 <https://github.com/coq/coq/pull/12682>`_,
+  by Hugo Herbelin).
+
+**Tactics**
+
+- **Fixed:**
+  :tacn:`typeclasses eauto` (and discriminated hint bases) now correctly
+  classify local variables as being unfoldable
+  (`#12572 <https://github.com/coq/coq/pull/12572>`_,
+  fixes `#12571 <https://github.com/coq/coq/issues/12571>`_,
+  by Pierre-Marie Pédrot).
+
+**Tactic language**
+
+- **Fixed:**
+  Excluding occurrences was causing an anomaly in tactics
+  (e.g., :g:`pattern _ at L` where :g:`L` is :g:`-2`).
+  (`#12541 <https://github.com/coq/coq/pull/12541>`_,
+  fixes `#12228 <https://github.com/coq/coq/issues/12228>`_,
+  by Pierre Roux).
+- **Fixed:**
+  Parsing of multi-parameters Ltac2 types
+  (`#12594 <https://github.com/coq/coq/pull/12594>`_,
+  fixes `#12595 <https://github.com/coq/coq/issues/12595>`_,
+  by Pierre-Marie Pédrot).
+
+**SSReflect**
+
+- **Fixed:**
+  Do not store the full environment inside ssr ast_closure_term
+  (`#12708 <https://github.com/coq/coq/pull/12708>`_,
+  fixes `#12707 <https://github.com/coq/coq/issues/12707>`_,
+  by Pierre-Marie Pédrot).
+
+**Commands and options**
+
+- **Fixed:**
+  Properly report the mismatched magic number of vo files
+  (`#12677 <https://github.com/coq/coq/pull/12677>`_,
+  fixes `#12513 <https://github.com/coq/coq/issues/12513>`_,
+  by Pierre-Marie Pédrot).
+- **Changed:**
+  Arbitrary hints have been undeprecated, and their definition
+  now triggers a standard warning instead
+  (`#12678 <https://github.com/coq/coq/pull/12678>`_,
+  fixes `#11970 <https://github.com/coq/coq/issues/11970>`_,
+  by Pierre-Marie Pédrot).
+
+**CoqIDE**
+
+- **Fixed:** CoqIDE no longer exits when trying to open a file whose name is not a valid identifier
+  (`#12562 <https://github.com/coq/coq/pull/12562>`_,
+  fixes `#10988 <https://github.com/coq/coq/issues/10988>`_,
+  by Vincent Laporte).
+
+**Infrastructure and dependencies**
+
+- **Fixed:**
+  Running ``make`` in ``test-suite/`` twice (or more) in a row will no longer
+  rebuild the ``modules/`` tests on subsequent runs, if they have not been
+  modified in the meantime (`#12583 <https://github.com/coq/coq/pull/12583>`_,
+  fixes `#12582 <https://github.com/coq/coq/issues/12582>`_, by Jason Gross).
+
 Version 8.11
 ------------