Release notes for 8.12.

123 files changed, 885 insertions, 828 deletions

diff --git a/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst b/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst
deleted file mode 100644
index 57bce7e4f6..0000000000
--- a/doc/changelog/02-specification-language/10202-master+fix8011-stronger-check-on-typability-ltac-env.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- **Changed:**
-  Warn when manual implicit arguments are used in unexpected positions
-  of a term (e.g. in `Check id (forall {x}, x)`) or when a implicit
-  argument name is shadowed (e.g. in `Check fun f : forall {x:nat}
-  {x}, nat => f`)
-  (`#10202 <https://github.com/coq/coq/pull/10202>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst b/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst
deleted file mode 100644
index 70c57c718f..0000000000
--- a/doc/changelog/02-specification-language/11098-master+arguments-supports-anonymous-implicit.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-- **Added:**
-  :cmd:`Arguments` now supports setting
-  implicit an anonymous argument, as e.g. in :g:`Arguments id {A} {_}`.
-  (`#11098 <https://github.com/coq/coq/pull/11098>`_,
-  by Hugo Herbelin, fixes `#4696
-  <https://github.com/coq/coq/pull/4696>`_, `#5173
-  <https://github.com/coq/coq/pull/5173>`_, `#9098
-  <https://github.com/coq/coq/pull/9098>`_).
diff --git a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst b/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
deleted file mode 100644
index 768ef68339..0000000000
--- a/doc/changelog/02-specification-language/11235-non_maximal_implicit.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Added:**
-  Syntax for non-maximal implicit arguments in definitions and terms using
-  square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]``
-  to be consistent with the command :cmd:`Arguments`.
-  (`#11235 <https://github.com/coq/coq/pull/11235>`_,
-  by SimonBoulier).
diff --git a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst b/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst
deleted file mode 100644
index 51818c666b..0000000000
--- a/doc/changelog/02-specification-language/11261-master+implicit-type-used-printing.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  :cmd:`Implicit Types` are now taken into account for printing. To inhibit it,
-  unset the :flag:`Printing Use Implicit Types` flag
-  (`#11261 <https://github.com/coq/coq/pull/11261>`_,
-  by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_).
diff --git a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst b/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst
deleted file mode 100644
index 66139f76e1..0000000000
--- a/doc/changelog/02-specification-language/11368-trailing_implicit_error.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Changed:**
-  The warning raised when a trailing implicit is declared to be non-maximally
-  inserted (with the command :cmd:`Arguments`) has been turned into an error.
-  This was deprecated since Coq 8.10
-  (`#11368 <https://github.com/coq/coq/pull/11368>`_,
-  by SimonBoulier).
diff --git a/doc/changelog/02-specification-language/11579-inductive-params.rst b/doc/changelog/02-specification-language/11579-inductive-params.rst
deleted file mode 100644
index 28bc8e9592..0000000000
--- a/doc/changelog/02-specification-language/11579-inductive-params.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- **Fixed:**
-  More robust and expressive treatment of implicit inductive
-  parameters in inductive declarations (`#11579
-  <https://github.com/coq/coq/pull/11579>`_, by Maxime Dénès, Gaëtan
-  Gilbert and Jasper Hugunin; fixes `#7253
-  <https://github.com/coq/coq/pull/7253>`_ and `#11585
-  <https://github.com/coq/coq/pull/11585>`_)
diff --git a/doc/changelog/02-specification-language/11600-uniform-syntax.rst b/doc/changelog/02-specification-language/11600-uniform-syntax.rst
deleted file mode 100644
index b95bad2eb8..0000000000
--- a/doc/changelog/02-specification-language/11600-uniform-syntax.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  New syntax :g:`Inductive Acc A R | x : Prop := ...` to specify which
-  parameters of an inductive are uniform.
-  See :ref:`parametrized-inductive-types`
-  (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst b/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst
deleted file mode 100644
index d69a94205f..0000000000
--- a/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  New warning on using :cmd:`Fixpoint` or :cmd:`CoFixpoint` for
-  definitions which are not recursive
-  (`#12121 <https://github.com/coq/coq/pull/12121>`_,
-  by Hugo Herbelin)
diff --git a/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst b/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst
deleted file mode 100644
index e5ec865b15..0000000000
--- a/doc/changelog/02-specification-language/12323-master+fix12322-anomaly-implicit-binder-factorization.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Fixed:**
-  Anomaly possibly raised when printing binders with implicit types
-  (`#12323 <https://github.com/coq/coq/pull/12323>`_,
-  by Hugo Herbelin; fixes `#12322 <https://github.com/coq/coq/pull/12322>`_).
diff --git a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst b/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst
deleted file mode 100644
index a8d4fc6ed2..0000000000
--- a/doc/changelog/03-notations/10832-master+fix6082-7766-overriding-notation-format.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Fixed:**
-  Different interpretations in different scopes of the same notation
-  string can now be associated to different printing formats (`#10832
-  <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin,
-  fixes `#6092 <https://github.com/coq/coq/issues/6092>`_
-  and `#7766 <https://github.com/coq/coq/issues/7766>`_).
diff --git a/doc/changelog/03-notations/11113-remove-compat.rst b/doc/changelog/03-notations/11113-remove-compat.rst
deleted file mode 100644
index 3bcdd3dd6f..0000000000
--- a/doc/changelog/03-notations/11113-remove-compat.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Removed:** deprecated ``compat`` modifier of :cmd:`Notation`
-  and :cmd:`Infix` commands
-  (`#11113 <https://github.com/coq/coq/pull/11113>`_,
-  by Théo Zimmermann, with help from Jason Gross).
diff --git a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
deleted file mode 100644
index eeb4c755f6..0000000000
--- a/doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
+++ /dev/null
@@ -1,17 +0,0 @@
-- **Fixed:** Parsing and printing consistently handle inheritance of implicit
-  arguments in notations. With the exception of notations of
-  the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which
-  inhibit implicit arguments, all notations binding a partially
-  applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`,
-  or :n:`Notation @string := (@@qualid {+ @arg })`, or
-  :n:`Notation @ident := (@qualid {+ @arg })`, or :n:`Notation @ident
-  := (@@qualid {+ @arg })`, inherit the remaining implicit arguments
-  (`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo
-  Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and
-  `#11091 <https://github.com/coq/coq/pull/11091>`_).
-
-- **Changed:** Notation scopes are now always inherited in
-  notations binding a partially applied constant, including for
-  notations binding an expression of the form :n:`@@qualid`. The latter was
-  not the case beforehand
-  (part of `#11120 <https://github.com/coq/coq/pull/11120>`_).
diff --git a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst b/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst
deleted file mode 100644
index f377b53ae2..0000000000
--- a/doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- **Changed:**
-  The printing algorithm now interleaves search for notations and removal of coercions
-  (`#11172 <https://github.com/coq/coq/pull/11172>`_, by Hugo Herbelin).
diff --git a/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst b/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst
deleted file mode 100644
index 1d94cbf21b..0000000000
--- a/doc/changelog/03-notations/11590-master+fix9741-only-printing-does-not-reserve-keyword.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Fixed:**
-  Notations in onlyprinting mode do not uselessly reserve parsing keywords
-  (`#11590 <https://github.com/coq/coq/pull/11590>`_,
-  by Hugo Herbelin, fixes `#9741 <https://github.com/coq/coq/pull/9741>`_).
diff --git a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst b/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst
deleted file mode 100644
index 1d30d16664..0000000000
--- a/doc/changelog/03-notations/11602-master+support-only-parsing-where-clause.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Added:**
-  Notations declared with the ``where`` clause in the declaration of
-  inductive types, coinductive types, record fields, fixpoints and
-  cofixpoints now support the ``only parsing`` modifier
-  (`#11602 <https://github.com/coq/coq/pull/11602>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/03-notations/11650-parensNew.rst b/doc/changelog/03-notations/11650-parensNew.rst
deleted file mode 100644
index f52a720428..0000000000
--- a/doc/changelog/03-notations/11650-parensNew.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  added the :flag:`Printing Parentheses` flag to print parentheses even when implied by associativity or precedence.
-  (`#11650 <https://github.com/coq/coq/pull/11650>`_,
-  by Hugo Herbelin and Abhishek Anand).
diff --git a/doc/changelog/03-notations/11848-nicer-decimal-printing.rst b/doc/changelog/03-notations/11848-nicer-decimal-printing.rst
deleted file mode 100644
index 1d3a390f36..0000000000
--- a/doc/changelog/03-notations/11848-nicer-decimal-printing.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  Nicer printing for decimal constants in R and Q.
-  1.5 is now printed 1.5 rather than 15e-1.
-  (`#11848 <https://github.com/coq/coq/pull/11848>`_,
-  by Pierre Roux).
diff --git a/doc/changelog/03-notations/11948-hexadecimal.rst b/doc/changelog/03-notations/11948-hexadecimal.rst
deleted file mode 100644
index e4b76d238c..0000000000
--- a/doc/changelog/03-notations/11948-hexadecimal.rst
+++ /dev/null
@@ -1,12 +0,0 @@
-- **Added:**
-  Numeral notations now parse hexadecimal constants such as ``0x2a``
-  or ``0xb.2ap-2``. Parsers added for :g:`nat`, :g:`positive`, :g:`Z`,
-  :g:`N`, :g:`Q`, :g:`R`, primitive integers and primitive floats
-  (`#11948 <https://github.com/coq/coq/pull/11948>`_,
-  by Pierre Roux).
-- **Deprecated:**
-  Numeral Notation on ``Decimal.uint``, ``Decimal.int`` and
-  ``Decimal.decimal`` are replaced respectively by numeral notations
-  on ``Numeral.uint``, ``Numeral.int`` and ``Numeral.numeral``
-  (`#11948 <https://github.com/coq/coq/pull/11948>`_,
-  by Pierre Roux).
diff --git a/doc/changelog/03-notations/12163-fix-12159.rst b/doc/changelog/03-notations/12163-fix-12159.rst
deleted file mode 100644
index 978ed561dd..0000000000
--- a/doc/changelog/03-notations/12163-fix-12159.rst
+++ /dev/null
@@ -1,11 +0,0 @@
-- **Fixed:**
-  Numeral Notations now play better with multiple scopes for the same
-  inductive type. Previously, when multiple numeral notations were defined
-  for the same inductive, only the last one was considered for
-  printing. Now, among the notations that are usable for printing and either
-  have a scope delimiter or are open, the selection is made according
-  to the order of open scopes, or according to the last defined
-  notation if no appropriate scope is open
-  (`#12163 <https://github.com/coq/coq/pull/12163>`_,
-  fixes `#12159 <https://github.com/coq/coq/pull/12159>`_,
-  by Pierre Roux, review by Hugo Herbelin and Jason Gross).
diff --git a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst
deleted file mode 100644
index e1fcfb78c4..0000000000
--- a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  Abbreviations support arguments occurring both in term and binder position
-  (`#8808 <https://github.com/coq/coq/pull/8808>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/04-tactics/10760-more-rapply.rst b/doc/changelog/04-tactics/10760-more-rapply.rst
deleted file mode 100644
index 32cd9b7135..0000000000
--- a/doc/changelog/04-tactics/10760-more-rapply.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-- **Changed:**
-  The tactic :tacn:`rapply` in :g:`Coq.Program.Tactics` now handles
-  arbitrary numbers of underscores and takes in a :g:`uconstr`.  In
-  rare cases where users were relying on :tacn:`rapply` inserting
-  exactly 15 underscores and no more, due to the lemma having a
-  completely unspecified codomain (and thus allowing for any number of
-  underscores), the tactic will now instead loop (`#10760
-  <https://github.com/coq/coq/pull/10760>`_, by Jason Gross).
diff --git a/doc/changelog/04-tactics/10998-zify-complements.rst b/doc/changelog/04-tactics/10998-zify-complements.rst
deleted file mode 100644
index ba4d10590f..0000000000
--- a/doc/changelog/04-tactics/10998-zify-complements.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-- **Added:**
-  The :tacn:`zify` tactic is now aware of `Pos.pred_double`, `Pos.pred_N`,
-  `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`,
-  `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, and `Z.quot2`.
-  Injections for internal definitions in module `ZifyBool` (`isZero` and `isLeZero`)
-  are also added to help users to declare new :tacn:`zify` class instances using
-  Micromega tactics
-  (`#10998 <https://github.com/coq/coq/pull/10998>`_, by Kazuhiko Sakaguchi).
diff --git a/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst
deleted file mode 100644
index d510416990..0000000000
--- a/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- **Changed:** The :g:`auto with zarith` tactic and variations (including :tacn:`intuition`)
-  may now call the :tacn:`lia` tactic instead of :tacn:`omega`
-  (when the `Omega` module is loaded);
-  more goals may be automatically solved,
-  fewer section variables will be captured spuriously
-  (`#11018 <https://github.com/coq/coq/pull/11018>`_,
-  by Vincent Laporte).
diff --git a/doc/changelog/04-tactics/11025-nativecompute-timing.rst b/doc/changelog/04-tactics/11025-nativecompute-timing.rst
deleted file mode 100644
index cb77457c31..0000000000
--- a/doc/changelog/04-tactics/11025-nativecompute-timing.rst
+++ /dev/null
@@ -1,11 +0,0 @@
-- **Changed:** The :flag:`NativeCompute Timing` flag causes calls to
-  :tacn:`native_compute` (as well as kernel calls to the native
-  compiler) to emit separate timing information about conversion to
-  native code, compilation, execution, and reification.  It replaces
-  the timing information previously emitted when the `-debug` flag was
-  set, and allows more fine-grained timing of the native compiler
-  (`#11025 <https://github.com/coq/coq/pull/11025>`_, by Jason Gross).
-  Additionally, the timing information now uses real time rather than
-  user time (Fixes `#11962
-  <https://github.com/coq/coq/issues/11962>`_, `#11963
-  <https://github.com/coq/coq/pull/11963>`_, by Jason Gross)
diff --git a/doc/changelog/04-tactics/11288-omega+depr.rst b/doc/changelog/04-tactics/11288-omega+depr.rst
deleted file mode 100644
index 3a2d421967..0000000000
--- a/doc/changelog/04-tactics/11288-omega+depr.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Removed:**
-  The undocumented ``omega with`` tactic variant has been removed,
-  using :tacn:`lia` is the recommended replacement, although the old semantics
-  of ``omega with *`` can also be recovered with ``zify; omega``
-  (`#11288 <https://github.com/coq/coq/pull/11288>`_,
-  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst
deleted file mode 100644
index 20d48929f2..0000000000
--- a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-- **Fixed:**
-  :tacn:`zify` now handles :g:`Z.pow_pos` by default.
-  In Coq 8.11, this was the case only when loading module
-  :g:`ZifyPow` because this triggered a regression of :tacn:`lia`.
-  The regression is now fixed, and the module kept only for compatibility
-  (`#11362 <https://github.com/coq/coq/pull/11362>`_,
-  fixes `#11191 <https://github.com/coq/coq/issues/11191>`_,
-  by Frédéric Besson).
diff --git a/doc/changelog/04-tactics/11370-zify-elim-let.rst b/doc/changelog/04-tactics/11370-zify-elim-let.rst
deleted file mode 100644
index 944dde99b8..0000000000
--- a/doc/changelog/04-tactics/11370-zify-elim-let.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- **Changed:**
-  Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml
-  (`#11370 <https://github.com/coq/coq/pull/11370>`_, by Frédéric Besson).
diff --git a/doc/changelog/04-tactics/11429-zify-optimisation.rst b/doc/changelog/04-tactics/11429-zify-optimisation.rst
deleted file mode 100644
index 25927f9182..0000000000
--- a/doc/changelog/04-tactics/11429-zify-optimisation.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- **Changed:**
-  Improve the efficiency of :tacn:`zify` by rewritting the remaining Ltac code in OCaml
-  (`#11429 <https://github.com/coq/coq/pull/11429>`_, by Frédéric Besson).
diff --git a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst
deleted file mode 100644
index 52a2b2f0f6..0000000000
--- a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-- **Added:**
-  :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls
-  (`#11474 <https://github.com/coq/coq/pull/11474>`_,  by Frédéric Besson).
-
-- **Fixed:**
-  Efficiency regression of :tacn:`lia`
-  (`#11474 <https://github.com/coq/coq/pull/11474>`_,
-  fixes `#11436 <https://github.com/coq/coq/issues/11436>`_,
-  by Frédéric Besson).
diff --git a/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst b/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst
deleted file mode 100644
index 3dd103b115..0000000000
--- a/doc/changelog/04-tactics/11522-master+pose-proof-wo-as-syntax.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Added:**
-  Syntax :n:`pose proof (@ident:=@term)` as an
-  alternative to :n:`pose proof @term as @ident`, following the model of
-  :n:`pose (@ident:=@term)`. See documentation of :tacn:`pose proof`
-  (`#11522 <https://github.com/coq/coq/pull/11522>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/04-tactics/11760-firstorder-leaf.rst b/doc/changelog/04-tactics/11760-firstorder-leaf.rst
deleted file mode 100644
index e6e4b827e5..0000000000
--- a/doc/changelog/04-tactics/11760-firstorder-leaf.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-- **Changed:**
-  The default tactic used by :g:`firstorder` is
-  :g:`auto with core` instead of :g:`auto with *`;
-  see :ref:`decisionprocedures` for details;
-  old behavior can be reset by using the `-compat 8.12` command-line flag;
-  to ease the migration of legacy code, the default solver can be set to `debug auto with *`
-  with `Set Firstorder Solver debug auto with *`
-  (`#11760 <https://github.com/coq/coq/pull/11760>`_,
-  by Vincent Laporte).
diff --git a/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst b/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst
deleted file mode 100644
index 827d484b28..0000000000
--- a/doc/changelog/04-tactics/11877-master+deprecated-_eqn.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Removed:**
-  Deprecated syntax `_eqn` for :tacn:`destruct` and :tacn:`remember`.
-  Use `eqn:` syntax instead
-  (`#11877 <https://github.com/coq/coq/pull/11877>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/04-tactics/11883-fix-autounfold.rst b/doc/changelog/04-tactics/11883-fix-autounfold.rst
deleted file mode 100644
index 83ff177380..0000000000
--- a/doc/changelog/04-tactics/11883-fix-autounfold.rst
+++ /dev/null
@@ -1,13 +0,0 @@
-- **Fixed:**
-  The behavior of :tacn:`autounfold` no longer depends on the names of terms and modules
-  (`#11883 <https://github.com/coq/coq/pull/11883>`_,
-  fixes `#7812 <https://github.com/coq/coq/issues/7812>`_,
-  by Attila Gáspár).
-- **Changed:**
-  `at` clauses can no longer be used with :tacn:`autounfold`. Since they had no effect, it is safe to remove them
-  (`#11883 <https://github.com/coq/coq/pull/11883>`_,
-  by Attila Gáspár).
-- **Changed:**
-  :tacn:`autounfold` no longer fails when the :cmd:`Opaque` command is used on constants in the hint databases
-  (`#11883 <https://github.com/coq/coq/pull/11883>`_,
-  by Attila Gáspár).
diff --git a/doc/changelog/04-tactics/11976-deprecate-omega.rst b/doc/changelog/04-tactics/11976-deprecate-omega.rst
deleted file mode 100644
index 59c9612d17..0000000000
--- a/doc/changelog/04-tactics/11976-deprecate-omega.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Deprecated:**
-  The :tacn:`omega` tactic is deprecated;
-  use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead
-  (`#11976 <https://github.com/coq/coq/pull/11976>`_,
-  by Vincent Laporte).
diff --git a/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst b/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst
deleted file mode 100644
index f10208e9b2..0000000000
--- a/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Changed:**
-  Tactics with qualified name of the form ``Coq.Init.Notations`` are
-  now qualified with prefix ``Coq.Init.Ltac``; users of the -noinit
-  option should now import Coq.Init.Ltac if they want to use Ltac
-  (`#12023 <https://github.com/coq/coq/pull/12023>`_,
-  by Hugo Herbelin; minor source of incompatibilities).
diff --git a/doc/changelog/04-tactics/12129-add-with-strategy.rst b/doc/changelog/04-tactics/12129-add-with-strategy.rst
deleted file mode 100644
index 68558c0cf4..0000000000
--- a/doc/changelog/04-tactics/12129-add-with-strategy.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  New tactical :tacn:`with_strategy` added which behaves like the
-  command :cmd:`Strategy`, with effects local to the given tactic
-  (`#12129 <https://github.com/coq/coq/pull/12129>`_, by Jason Gross).
diff --git a/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst
deleted file mode 100644
index 055006d3b4..0000000000
--- a/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-- **Changed:**
-  Tactic :tacn:`subst` :n:`@ident` now fails over a section variable which is
-  indirectly dependent in the goal; the incompatibility can generally
-  be fixed by first clearing the hypotheses causing an indirect
-  dependency, as reported by the error message, or by using :tacn:`rewrite` :n:`in *`
-  instead; similarly, :tacn:`subst` has no more effect on such variables
-  (`#12146 <https://github.com/coq/coq/pull/12146>`_,
-  by Hugo Herbelin; fixes `#10812 <https://github.com/coq/coq/pull/10812>`_;
-  fixes `#12139 <https://github.com/coq/coq/pull/12139>`_).
diff --git a/doc/changelog/04-tactics/12213-zify-Nat.rst b/doc/changelog/04-tactics/12213-zify-Nat.rst
deleted file mode 100644
index 8b744cd193..0000000000
--- a/doc/changelog/04-tactics/12213-zify-Nat.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- **Added:**
-  The :tacn:`zify` tactic is now aware of `Nat.le`, `Nat.lt` and `Nat.eq`
-  (`#12213 <https://github.com/coq/coq/pull/12213>`_, by Frédéric Besson; fixes `#12210 <https://github.com/coq/coq/issues/12210>`_).
diff --git a/doc/changelog/04-tactics/12256-unfold-dyn-check.rst b/doc/changelog/04-tactics/12256-unfold-dyn-check.rst
deleted file mode 100644
index c2f7065f4c..0000000000
--- a/doc/changelog/04-tactics/12256-unfold-dyn-check.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Changed:**
-  The check that unfold arguments were indeed unfoldable has been moved to runtime
-  (`#12256 <https://github.com/coq/coq/pull/12256>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/04-tactics/12326-fix11761-functional-induction-throws-unrecoverable-error.rst b/doc/changelog/04-tactics/12326-fix11761-functional-induction-throws-unrecoverable-error.rst
deleted file mode 100644
index 2402321fad..0000000000
--- a/doc/changelog/04-tactics/12326-fix11761-functional-induction-throws-unrecoverable-error.rst
+++ /dev/null
@@ -1,13 +0,0 @@
-- **Fixed:**
-  Wrong type error in tactic :tacn:`functional induction`.
-  (`#12326 <https://github.com/coq/coq/pull/12326>`_,
-  by Pierre Courtieu,
-  fixes `#11761 <https://github.com/coq/coq/issues/11761>`_,
-  reported by Lasse Blaauwbroek).
-- **Changed**
-  When the tactic :tacn:`functional induction` :n:`c__1 c__2 ... c__n` is used
-  with no parenthesis around :n:`c__1 c__2 ... c__n`, :n:`c__1 c__2 ... c__n` is now
-  read as one sinlge applicative term. In particular implicit
-  arguments should be omitted. Rare source of incompatibility
-  (`#12326 <https://github.com/coq/coq/pull/12326>`_,
-  by Pierre Courtieu).
diff --git a/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst b/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst
deleted file mode 100644
index e8233b9d13..0000000000
--- a/doc/changelog/05-tactic-language/10343-issue-10342-ltac2-standard-library.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  An array library for Ltac2 (as compatible as possible with OCaml standard library)
-  (`#10343 <https://github.com/coq/coq/pull/10343>`_,
-  by Michael Soegtrop).
diff --git a/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst
deleted file mode 100644
index 0dd0fed4e2..0000000000
--- a/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Added:**
-  The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to
-  give a name to the old value so as to be able to reuse it inside the
-  new one
-  (`#11503 <https://github.com/coq/coq/pull/11503>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/05-tactic-language/11740-ltac2-enough.rst b/doc/changelog/05-tactic-language/11740-ltac2-enough.rst
deleted file mode 100644
index 5d3671bce1..0000000000
--- a/doc/changelog/05-tactic-language/11740-ltac2-enough.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  Ltac2 notations for :tacn:`enough` and :tacn:`eenough`
-  (`#11740 <https://github.com/coq/coq/pull/11740>`_,
-  by Michael Soegtrop).
diff --git a/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst b/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst
deleted file mode 100644
index 47e7be4d0e..0000000000
--- a/doc/changelog/05-tactic-language/11882-master+ltac2-fresh-in-context.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Added:**
-  New Ltac2 function ``Fresh.Free.of_goal`` to return the list of
-  names of declarations of the current goal; new Ltac2 function
-  ``Fresh.in_goal`` to return a variable fresh in the current goal
-  (`#11882 <https://github.com/coq/coq/pull/11882>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst b/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst
deleted file mode 100644
index 2f8d92fae5..0000000000
--- a/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  Ltac2 notations for reductions in terms: :n:`eval @red_expr in @ltac2_term`
-  (`#11981 <https://github.com/coq/coq/pull/11981>`_,
-  by Michael Soegtrop).
diff --git a/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst b/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst
deleted file mode 100644
index b90c8e7a1f..0000000000
--- a/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-- **Fixed:**
-  The :flag:`Ltac Profiling` machinery now correctly handles
-  backtracking into multi-success tactics.  The call-counts of some
-  tactics are unfortunately inflated by 1, as some tactics are
-  implicitly implemented as :g:`tac + fail`, which has two
-  entry-points rather than one (Fixes `#12196
-  <https://github.com/coq/coq/issues/12196>`_, `#12197
-  <https://github.com/coq/coq/pull/12197>`_, by Jason Gross).
diff --git a/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst b/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst
deleted file mode 100644
index 69632fd202..0000000000
--- a/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  The "reference" tactic generic argument now accepts arbitrary
-  variables of the goal context
-  (`#12254 <https://github.com/coq/coq/pull/12254>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/06-ssreflect/8855-master+more-search-options.rst b/doc/changelog/06-ssreflect/8855-master+more-search-options.rst
deleted file mode 100644
index 2fdacfd82a..0000000000
--- a/doc/changelog/06-ssreflect/8855-master+more-search-options.rst
+++ /dev/null
@@ -1,11 +0,0 @@
-- **Changed:** The :cmd:`Search (ssreflect)` command that used to be
-  available when loading the `ssreflect` plugin has been moved to a
-  separate plugin that needs to be loaded separately: `ssrsearch`
-  (part of `#8855 <https://github.com/coq/coq/pull/8855>`_, fixes
-  `#12253 <https://github.com/coq/coq/issues/12253>`_, by Théo
-  Zimmermann).
-
-- **Deprecated:** :cmd:`Search (ssreflect)` (available through
-  `Require ssrsearch.`) in favor of the `headconcl:` clause of
-  :cmd:`Search` (part of `#8855
-  <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann).
diff --git a/doc/changelog/07-commands-and-options/07791-deprecate-hint-constr.rst b/doc/changelog/07-commands-and-options/07791-deprecate-hint-constr.rst
deleted file mode 100644
index b627fdbcc9..0000000000
--- a/doc/changelog/07-commands-and-options/07791-deprecate-hint-constr.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Deprecated:**
-  Deprecated the declaration of arbitrary terms as hints. Global
-  references are now preferred
-  (`#7791 <https://github.com/coq/coq/pull/7791>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst b/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst
deleted file mode 100644
index b263de017b..0000000000
--- a/doc/changelog/07-commands-and-options/10747-canonical-better-message.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  The :cmd:`Print Canonical Projections` command can now take constants and
-  prints only the unification rules that involve or are synthesized from given
-  constants (`#10747 <https://github.com/coq/coq/pull/10747>`_,
-  by Kazuhiko Sakaguchi).
diff --git a/doc/changelog/07-commands-and-options/11162-local-cs.rst b/doc/changelog/07-commands-and-options/11162-local-cs.rst
deleted file mode 100644
index b89e047153..0000000000
--- a/doc/changelog/07-commands-and-options/11162-local-cs.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- **Added:** Handle the :attr:`local` attribute in :cmd:`Canonical
-  Structure` declarations (`#11162
-  <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi).
diff --git a/doc/changelog/07-commands-and-options/11164-let-cs.rst b/doc/changelog/07-commands-and-options/11164-let-cs.rst
deleted file mode 100644
index 2bdc8052c6..0000000000
--- a/doc/changelog/07-commands-and-options/11164-let-cs.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- **Added:** A section variable introduced with :cmd:`Let` can be
-  declared as a :cmd:`Canonical Structure` (`#11164
-  <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi).
diff --git a/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst b/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst
deleted file mode 100644
index 9fc09c4189..0000000000
--- a/doc/changelog/07-commands-and-options/11185-remove-typeclasses-axioms-instances.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- **Removed:** ``Typeclasses Axioms Are Instances`` flag, deprecated since 8.10.
-  Use :cmd:`Declare Instance` for axioms which should be instances
-  (`#11185 <https://github.com/coq/coq/pull/11185>`_, by Théo Zimmermann).
diff --git a/doc/changelog/07-commands-and-options/11258-coherence.rst b/doc/changelog/07-commands-and-options/11258-coherence.rst
deleted file mode 100644
index f04a120417..0000000000
--- a/doc/changelog/07-commands-and-options/11258-coherence.rst
+++ /dev/null
@@ -1,10 +0,0 @@
-- **Changed:**
-  The :cmd:`Coercion` command has been improved to check the coherence of the
-  inheritance graph. It checks whether a circular inheritance path of `C >-> C`
-  is convertible with the identity function or not, then report it as an
-  ambiguous path if it is not.  The new mechanism does not report ambiguous
-  paths that are redundant with others. For example, checking the ambiguity of
-  `[f; g]` and `[f'; g]` is redundant with that of `[f]` and `[f']` thus will
-  not be reported
-  (`#11258 <https://github.com/coq/coq/pull/11258>`_,
-  by Kazuhiko Sakaguchi).
diff --git a/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst b/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst
deleted file mode 100644
index 7bcbb9a8e3..0000000000
--- a/doc/changelog/07-commands-and-options/11534-let-with-annotations.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- **Added:** Support for universe bindings and universe contrainsts in
-  :cmd:`Let` definitions (`#11534
-  <https://github.com/coq/coq/pull/11534>`_, by Théo Zimmermann).
diff --git a/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst b/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst
deleted file mode 100644
index d134aeae8b..0000000000
--- a/doc/changelog/07-commands-and-options/11546-rm-uncheck-template.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Removed:** Deprecated unsound compatibility ``Template Check``
-  flag that was introduced in 8.10 to help users gradually move their
-  template polymorphic inductive type definitions outside sections
-  (`#11546 <https://github.com/coq/coq/pull/11546>`_, by Pierre-Marie
-  Pédrot).
diff --git a/doc/changelog/07-commands-and-options/11618-loadpath+split_ml_handling.rst b/doc/changelog/07-commands-and-options/11618-loadpath+split_ml_handling.rst
deleted file mode 100644
index 99f2d22d11..0000000000
--- a/doc/changelog/07-commands-and-options/11618-loadpath+split_ml_handling.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-- **Removed:**
-  Recursive OCaml loadpaths are not supported anymore; the command
-  ``Add Rec ML Path`` has been removed; :cmd:`Add ML Path` is now the
-  preferred one. We have also dropped support for the non-qualified
-  version of the :cmd:`Add LoadPath` command, that is to say,
-  the ``Add LoadPath dir`` version; now,
-  you must always specify a prefix now using ``Add Loadpath dir as Prefix``
-  (`#11618 <https://github.com/coq/coq/pull/11618>`_,
-  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst
deleted file mode 100644
index 419d683037..0000000000
--- a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Removed:**
-  Unqualified ``polymorphic``, ``monomorphic``, ``template``,
-  ``notemplate`` attributes (they were deprecated since Coq 8.10).
-  Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
-  :attr:`universes(template)` and :attr:`universes(notemplate)` instead
-  (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann).
diff --git a/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst
deleted file mode 100644
index 7b690da68d..0000000000
--- a/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst
+++ /dev/null
@@ -1,11 +0,0 @@
-- **Added:**
-  New attributes supported when defining an inductive type
-  :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and
-  :attr:`private(matching)`, which correspond to legacy attributes
-  ``Cumulative``, ``NonCumulative``, and the so far undocumented
-  ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by
-  Théo Zimmermann).
-
-- **Changed:** :term:`Legacy attributes <attribute>` can now be passed
-  in any order (`#11665 <https://github.com/coq/coq/pull/11665>`_, by
-  Théo Zimmermann).
diff --git a/doc/changelog/07-commands-and-options/11746-remove-chapter.rst b/doc/changelog/07-commands-and-options/11746-remove-chapter.rst
deleted file mode 100644
index 0316432b0a..0000000000
--- a/doc/changelog/07-commands-and-options/11746-remove-chapter.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- **Removed:** undocumented ``Chapter`` command.  Use :cmd:`Section`
-  instead (`#11746 <https://github.com/coq/coq/pull/11746>`_, by Théo
-  Zimmermann).
diff --git a/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst b/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst
deleted file mode 100644
index 5b0cdb5914..0000000000
--- a/doc/changelog/07-commands-and-options/11795-print_implicit_args.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  Several commands (`Search`, `About`, ...) now print the implicit arguments
-  in brackets when printing types.
-  (`#11795 <https://github.com/coq/coq/pull/11795>`_,
-  by SimonBoulier).
diff --git a/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst b/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst
deleted file mode 100644
index 9341eebb58..0000000000
--- a/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  the :cmd:`Hint` commands now accept the :attr:`export` locality as
-  an attribute, allowing to make import-scoped hints
-  (`#11812 <https://github.com/coq/coq/pull/11812>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst b/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst
deleted file mode 100644
index 5ab2941446..0000000000
--- a/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-- **Deprecated:**
-  Option :flag:`Hide Obligations` has been deprecated
-  (`#11828 <https://github.com/coq/coq/pull/11828>`_,
-  by Emilio Jesus Gallego Arias).
-
-- **Removed:**
-  Deprecated option ``Shrink Obligations`` has been removed
-  (`#11828 <https://github.com/coq/coq/pull/11828>`_,
-  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst
deleted file mode 100644
index e409c638bb..0000000000
--- a/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-- **Removed:** Removed SearchAbout command that was deprecated in 8.5.
-  Use :cmd:`Search` instead.
-  (`#11944 <https://github.com/coq/coq/pull/11944>`_, by Jim Fehrle).
diff --git a/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst
deleted file mode 100644
index ad7cf44482..0000000000
--- a/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  Added :flag:`Cumulative StrictProp` to control cumulativity of
-  |SProp| and deprecated now redundant command line
-  ``--cumulative-sprop`` (`#12034
-  <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst b/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst
deleted file mode 100644
index 259253ec79..0000000000
--- a/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Fixed:**
-  A printing bug in the presence of elimination principles with local definitions
-  (`#12295 <https://github.com/coq/coq/pull/12295>`_,
-  by Hugo Herbelin; fixes `#12233 <https://github.com/coq/coq/pull/12233>`_).
diff --git a/doc/changelog/07-commands-and-options/12296-master+fix12234-show-proof-proper.rst b/doc/changelog/07-commands-and-options/12296-master+fix12234-show-proof-proper.rst
deleted file mode 100644
index dc71a27eb8..0000000000
--- a/doc/changelog/07-commands-and-options/12296-master+fix12234-show-proof-proper.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  Anomalies with :cmd:`Show Proof`
-  (`#12296 <https://github.com/coq/coq/pull/12296>`_,
-  by Hugo Herbelin; fixes
-  `#12234 <https://github.com/coq/coq/pull/12234>`_).
diff --git a/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst
deleted file mode 100644
index 5b35090d7e..0000000000
--- a/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  :cmd:Redirect now obeys the :opt:`Printing Width` and
-  :opt:`Printing Depth` flags.
-  (`#12358 <https://github.com/coq/coq/pull/12358>`_,
-  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst b/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst
deleted file mode 100644
index cd993bf356..0000000000
--- a/doc/changelog/07-commands-and-options/8855-master+more-search-options.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-- **Added:** Support for new clauses `hyp:`, `headhyp:`, `concl:`,
-  `headconcl:`, `head:` and `is:` in :cmd:`Search`.  Support for
-  complex search queries combining disjunctions, conjunctions and
-  negations (`#8855 <https://github.com/coq/coq/pull/8855>`_, by Hugo
-  Herbelin, with ideas from Cyril Cohen and help from Théo
-  Zimmermann).
-- **Deprecated:** :cmd:`SearchHead` in favor of the new `headconcl:`
-  clause of :cmd:`Search` (part of `#8855
-  <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann).
diff --git a/doc/changelog/08-tools/10592-coqdoc-details.rst b/doc/changelog/08-tools/10592-coqdoc-details.rst
deleted file mode 100644
index c5bdc1dbb0..0000000000
--- a/doc/changelog/08-tools/10592-coqdoc-details.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  A new documentation environment ``details`` to make certain portion
-  of a Coq document foldable.  See :ref:`coqdoc`
-  (`#10592 <https://github.com/coq/coq/pull/10592>`_,
-  by Thomas Letan).
diff --git a/doc/changelog/08-tools/11302-better-timing-scripts-options.rst b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst
deleted file mode 100644
index 3b20bbf75d..0000000000
--- a/doc/changelog/08-tools/11302-better-timing-scripts-options.rst
+++ /dev/null
@@ -1,35 +0,0 @@
-- **Added:**
-  The ``make-both-single-timing-files.py`` script now accepts a
-  ``--fuzz=N`` parameter on the command line which determines how many
-  characters two lines may be offset in the "before" and "after"
-  timing logs while still being considered the same line.  When
-  invoking this script via the ``print-pretty-single-time-diff``
-  target in a ``Makefile`` made by ``coq_makefile``, you can set this
-  argument by passing ``TIMING_FUZZ=N`` to ``make`` (`#11302
-  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
-
-- **Added:**
-  The ``make-one-time-file.py`` and ``make-both-time-files.py``
-  scripts now accept a ``--real`` parameter on the command line to
-  print real times rather than user times in the tables.  The
-  ``make-both-single-timing-files.py`` script accepts a ``--user``
-  parameter to use user times.  When invoking these scripts via the
-  ``print-pretty-timed`` or ``print-pretty-timed-diff`` or
-  ``print-pretty-single-time-diff`` targets in a ``Makefile`` made by
-  ``coq_makefile``, you can set this argument by passing
-  ``TIMING_REAL=1`` (to pass ``--real``) or ``TIMING_REAL=0`` (to pass
-  ``--user``) to ``make`` (`#11302
-  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
-
-- **Added:**
-  Coq's build system now supports both ``TIMING_FUZZ``,
-  ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile``
-  made by ``coq_makefile`` (`#11302
-  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
-
-- **Fixed:**
-  The various timing targets for Coq's standard library now correctly
-  display and label the "before" and "after" columns, rather than
-  mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_
-  fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason
-  Gross).
diff --git a/doc/changelog/08-tools/11409-mltop+deprecate_use.rst b/doc/changelog/08-tools/11409-mltop+deprecate_use.rst
deleted file mode 100644
index f4f110ed67..0000000000
--- a/doc/changelog/08-tools/11409-mltop+deprecate_use.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Removed:**
-  The `-load-ml-source` and `-load-ml-object` command line options
-  have been removed; their use was very limited, you can achieve the same adding
-  additional object files in the linking step or using a plugin
-  (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/08-tools/11523-coqdep+refactor2.rst b/doc/changelog/08-tools/11523-coqdep+refactor2.rst
deleted file mode 100644
index 3f93d60926..0000000000
--- a/doc/changelog/08-tools/11523-coqdep+refactor2.rst
+++ /dev/null
@@ -1,10 +0,0 @@
-- **Changed:**
-  Internal options and behavior of ``coqdep`` have changed. ``coqdep``
-  no longer works as a replacement for ``ocamldep``, thus ``.ml``
-  files are not supported as input. Also, several deprecated options
-  have been removed: ``-w``, ``-D``, ``-mldep``, ``-prefix``,
-  ``-slash``, and ``-dumpbox``. Passing ``-boot`` to ``coqdep`` will
-  not load any path by default now, ``-R/-Q`` should be used instead
-  (`#11523 <https://github.com/coq/coq/pull/11523>`_ and
-  `#11589 <https://github.com/coq/coq/pull/11589>`_,
-  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/08-tools/11606-memory-in-timing-scripts.rst b/doc/changelog/08-tools/11606-memory-in-timing-scripts.rst
deleted file mode 100644
index e09c6ef3a3..0000000000
--- a/doc/changelog/08-tools/11606-memory-in-timing-scripts.rst
+++ /dev/null
@@ -1,25 +0,0 @@
-- **Added:**
-  The ``make-one-time-file.py`` and ``make-both-time-files.py``
-  scripts now include peak memory usage information in the tables (can
-  be turned off by the ``--no-include-mem`` command-line parameter),
-  and a ``--sort-by-mem`` parameter to sort the tables by memory
-  rather than time.  When invoking these scripts via the
-  ``print-pretty-timed`` or ``print-pretty-timed-diff`` targets in a
-  ``Makefile`` made by ``coq_makefile``, you can set this argument by
-  passing ``TIMING_INCLUDE_MEM=0`` (to pass ``--no-include-mem``) and
-  ``TIMING_SORT_BY_MEM=1`` (to pass ``--sort-by-mem``) to ``make``
-  (`#11606 <https://github.com/coq/coq/pull/11606>`_, by Jason Gross).
-
-- **Added:**
-  Coq's build system now supports both ``TIMING_INCLUDE_MEM`` and
-  ``TIMING_SORT_BY_MEM`` just like a ``Makefile`` made by
-  ``coq_makefile`` (`#11606 <https://github.com/coq/coq/pull/11606>`_,
-  by Jason Gross).
-
-- **Changed:**
-  The sorting order of the timing script ``make-both-time-files.py``
-  and the target ``print-pretty-timed-diff`` is now deterministic even
-  when the sorting order is ``absolute`` or ``diff``; previously the
-  relative ordering of two files with identical times was
-  non-deterministic (`#11606
-  <https://github.com/coq/coq/pull/11606>`_, by Jason Gross).
diff --git a/doc/changelog/08-tools/11617-toplevel+boot.rst b/doc/changelog/08-tools/11617-toplevel+boot.rst
deleted file mode 100644
index 49dd0ee2d8..0000000000
--- a/doc/changelog/08-tools/11617-toplevel+boot.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  New ``coqc`` / ``coqtop`` option ``-boot`` that will not bind the
-  `Coq` library prefix by default
-  (`#11617 <https://github.com/coq/coq/pull/11617>`_,
-  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
deleted file mode 100644
index ff736641b4..0000000000
--- a/doc/changelog/08-tools/11851-coqc-flags-fix.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-- **Changed:**
-  The order in which the require flags `-ri`, `-re`, `-rfrom`, etc.
-  and the option flags `-set`, `-unset` are given now matters.  In
-  particular, it is now possible to interleave the loading of plugins
-  and the setting of options by choosing the right order for these
-  flags.  The load flags `-l` and `-lv` are still processed afterward
-  for now (`#11851 <https://github.com/coq/coq/pull/11851>`_ and
-  `#12097 <https://github.com/coq/coq/pull/12097>`_,
-  by Lasse Blaauwbroek).
diff --git a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst
deleted file mode 100644
index affb685fcb..0000000000
--- a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Removed:**
-  Confusingly-named and deprecated since 8.11 `-require` option.
-  Use the equivalent `-require-import` instead
-  (`#12005 <https://github.com/coq/coq/pull/12005>`_,
-  by Théo Zimmermann).
diff --git a/doc/changelog/08-tools/12006-issue5632.rst b/doc/changelog/08-tools/12006-issue5632.rst
deleted file mode 100644
index 162d56b1b6..0000000000
--- a/doc/changelog/08-tools/12006-issue5632.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  ``Makefile`` generated by ``coq_makefile`` erases ``.lia.cache`` and ``.nia.cache`` by ``make cleanall``.
-  (`#12006 <https://github.com/coq/coq/pull/12006>`_,
-  by Olivier Laurent).
diff --git a/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst b/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst
deleted file mode 100644
index 5c4ef82b8b..0000000000
--- a/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  Definitions in coqdoc link to themselves, giving access in html to their own url
-  (`#12026 <https://github.com/coq/coq/pull/12026>`_,
-  by Hugo Herbelin; granting `#7093 <https://github.com/coq/coq/pull/7093>`_).
diff --git a/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst b/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst
deleted file mode 100644
index ae9b69e592..0000000000
--- a/doc/changelog/08-tools/12027-master+fix3415-coqdoc-record.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  Fields of a record tuple now link in coqdoc to their definition
-  (`#12027 <https://github.com/coq/coq/pull/12027>`_, fixes
-  `#3415 <https://github.com/coq/coq/issues/3415>`_,
-  by Hugo Herbelin; ).
diff --git a/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst b/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst
deleted file mode 100644
index af0d28305a..0000000000
--- a/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  Add hyperlinks on bound variables for coqdoc
-  (`#12033 <https://github.com/coq/coq/pull/12033>`_,
-  by Hugo Herbelin; it incidentally fixes
-  `#7697 <https://github.com/coq/coq/pull/7697>`_).
diff --git a/doc/changelog/08-tools/12037-coqdoc-preformatted.rst b/doc/changelog/08-tools/12037-coqdoc-preformatted.rst
deleted file mode 100644
index bf65719516..0000000000
--- a/doc/changelog/08-tools/12037-coqdoc-preformatted.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Fixed:**
-  ``coqdoc`` now reports the location of a mismatched opening ``[[`` instead of
-  throwing an uninformative exception.
-  (`#12037 <https://github.com/coq/coq/pull/12037>`_,
-  fixes `#9670 <https://github.com/coq/coq/issues/9670>`_,
-  by Lysxia).
diff --git a/doc/changelog/08-tools/12076-fix-5030.rst b/doc/changelog/08-tools/12076-fix-5030.rst
deleted file mode 100644
index afb59b1cde..0000000000
--- a/doc/changelog/08-tools/12076-fix-5030.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Fixed:**
-  Fix #5030 (coqchk reports names from opaque modules as axioms)
-  (`#12076 <https://github.com/coq/coq/pull/12076>`_,
-  by Pierre Roux).
diff --git a/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst b/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst
deleted file mode 100644
index f6af5d40e8..0000000000
--- a/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  ``Coqdoc``: Highlighting of the exact position of the target of links
-  (`#12091 <https://github.com/coq/coq/pull/12091>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/08-tools/12126-adjust-timed-name.rst b/doc/changelog/08-tools/12126-adjust-timed-name.rst
deleted file mode 100644
index c305b384d9..0000000000
--- a/doc/changelog/08-tools/12126-adjust-timed-name.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-- **Changed:**
-  The output of ``make TIMED=1`` (and therefore the timing targets
-  such as ``print-pretty-timed`` and ``print-pretty-timed-diff``) now
-  displays the full name of the output file being built, rather than
-  the stem of the rule (which was usually the filename without the
-  extension, but in general could be anything for user-defined rules
-  involving ``%``) (`#12126
-  <https://github.com/coq/coq/pull/12126>`_, by Jason Gross).
diff --git a/doc/changelog/08-tools/12211-time-ocaml.rst b/doc/changelog/08-tools/12211-time-ocaml.rst
deleted file mode 100644
index 7ff68cc495..0000000000
--- a/doc/changelog/08-tools/12211-time-ocaml.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  When passing ``TIMED=1`` to ``make`` with either Coq's own makefile
-  or a ``coq_makefile``\-made makefile, timing information is now
-  printed for OCaml files as well (`#12211
-  <https://github.com/coq/coq/pull/12211>`_, by Jason Gross).
diff --git a/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst b/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst
deleted file mode 100644
index 8a43f5af94..0000000000
--- a/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Changed:**
-  The pretty-timed scripts and targets now print a newline at the end of their
-  tables, rather than creating text with no trailing newline (`#12368
-  <https://github.com/coq/coq/pull/12368>`_, by Jason Gross).
diff --git a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst
deleted file mode 100644
index 49ac16eee9..0000000000
--- a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Removed:**
-  "Tactic" menu from CoqIDE which had been unmaintained for a number of years
-  (`#11414 <https://github.com/coq/coq/pull/11414>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst b/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst
deleted file mode 100644
index 9d22a858f1..0000000000
--- a/doc/changelog/09-coqide/11415-remove-ide-revert-all-buffers.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Removed:**
-  "Revert all buffers" command from CoqIDE which had been broken for a long time
-  (`#11415 <https://github.com/coq/coq/pull/11415>`_,
-  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/10-standard-library/11127-trunk.rst b/doc/changelog/10-standard-library/11127-trunk.rst
deleted file mode 100644
index 3f461397ae..0000000000
--- a/doc/changelog/10-standard-library/11127-trunk.rst
+++ /dev/null
@@ -1,2 +0,0 @@
-- **Added:** Theorem :g:`bezout_comm` for natural numbers
-  (`#11127 <https://github.com/coq/coq/pull/11127>`_, by Daniel de Rauglaudre).
diff --git a/doc/changelog/10-standard-library/11240-rew-dependent.rst b/doc/changelog/10-standard-library/11240-rew-dependent.rst
deleted file mode 100644
index e9daab0c2c..0000000000
--- a/doc/changelog/10-standard-library/11240-rew-dependent.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added**
-  Added :g:`rew dependent` notations for the dependent version of
-  :g:`rew` in :g:`Coq.Init.Logic.EqNotations` to improve the display
-  and parsing of :g:`match` statements on :g:`Logic.eq` (`#11240
-  <https://github.com/coq/coq/pull/11240>`_, by Jason Gross).
diff --git a/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst b/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst
deleted file mode 100644
index be54e45808..0000000000
--- a/doc/changelog/10-standard-library/11249-ollibs-list-changelog.rst
+++ /dev/null
@@ -1,18 +0,0 @@
-- **Added:**
-  lemmas about lists:
-
-  - properties of ``In``: ``in_elt``, ``in_elt_inv``
-  - properties of ``nth``: ``app_nth2_plus``, ``nth_middle``, ``nth_ext``
-  - properties of ``last``: ``last_last``, ``removelast_last``
-  - properties of ``remove``: ``remove_cons``, ``remove_app``, ``notin_remove``, ``in_remove``, ``in_in_remove``, ``remove_remove_comm``, ``remove_remove_eq``, ``remove_length_le``, ``remove_length_lt``
-  - properties of ``concat``: ``in_concat``, ``remove_concat``
-  - properties of ``map`` and ``flat_map``: ``map_last``, ``map_eq_cons``, ``map_eq_app``, ``flat_map_app``, ``flat_map_ext``, ``nth_nth_nth_map``
-  - properties of ``incl``: ``incl_nil_l``, ``incl_l_nil``, ``incl_cons_inv``, ``incl_app_app``, ``incl_app_inv``, ``remove_incl``, ``incl_map``, ``incl_filter``, ``incl_Forall_in_iff``
-  - properties of ``NoDup`` and ``nodup``: ``NoDup_rev``, ``NoDup_filter``, ``nodup_incl``
-  - properties of ``Exists`` and ``Forall``: ``Exists_nth``, ``Exists_app``, ``Exists_rev``, ``Exists_fold_right``, ``incl_Exists``, ``Forall_nth``, ``Forall_app``, ``Forall_elt``, ``Forall_rev``, ``Forall_fold_right``, ``incl_Forall``, ``map_ext_Forall``, ``Exists_or``, ``Exists_or_inv``, ``Forall_and``, ``Forall_and_inv``, ``exists_Forall``, ``Forall_image``, ``concat_nil_Forall``, ``in_flat_map_Exists``, ``notin_flat_map_Forall``
-  - properties of ``repeat``: ``repeat_cons``, ``repeat_to_concat``
-  - definitions and properties of ``list_sum`` and ``list_max``: ``list_sum_app``, ``list_max_app``, ``list_max_le``, ``list_max_lt``
-  - misc: ``elt_eq_unit``, ``last_length``, ``rev_eq_app``, ``removelast_firstn_len``, ``cons_seq``, ``seq_S``
-
-  (`#11249 <https://github.com/coq/coq/pull/11249>`_, `#12237 <https://github.com/coq/coq/pull/12237>`_,
-  by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/11335-ollibs-wfnat-changelog.rst b/doc/changelog/10-standard-library/11335-ollibs-wfnat-changelog.rst
deleted file mode 100644
index 0eb3eefde5..0000000000
--- a/doc/changelog/10-standard-library/11335-ollibs-wfnat-changelog.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  Well-founded induction principles for `nat`: ``lt_wf_rect1``, ``lt_wf_rect``, ``gt_wf_rect``, ``lt_wf_double_rect``
-  (`#11335 <https://github.com/coq/coq/pull/11335>`_,
-  by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/11350-list.rst b/doc/changelog/10-standard-library/11350-list.rst
deleted file mode 100644
index 52c2517161..0000000000
--- a/doc/changelog/10-standard-library/11350-list.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  ``remove'`` and ``count_occ'`` over lists,
-  alternatives to ``remove`` and ``count_occ`` based on ``filter``
-  (`#11350 <https://github.com/coq/coq/pull/11350>`_,
-  by Yishuai Li).
diff --git a/doc/changelog/10-standard-library/11404-removeRList.rst b/doc/changelog/10-standard-library/11404-removeRList.rst
deleted file mode 100644
index 88e22d128c..0000000000
--- a/doc/changelog/10-standard-library/11404-removeRList.rst
+++ /dev/null
@@ -1,15 +0,0 @@
-- **Removed:**
-  Type `RList` has been removed.  All uses have been replaced by `list R`.
-  Functions from `RList` named `In`, `Rlength`, `cons_Rlist`, `app_Rlist`
-  have also been removed as they are essentially the same as `In`, `length`,
-  `app`, and `map` from `List`, modulo the following changes:
-
-    - `RList.In x (RList.cons a l)` used to be convertible to
-      `(x = a) \\/ RList.In x l`,
-      but `List.In x (a :: l)` is convertible to
-      `(a = x) \\/ List.In l`.
-      The equality is reversed.
-    - `app_Rlist` and `List.map` take arguments in different order.
-
-  (`#11404 <https://github.com/coq/coq/pull/11404>`_,
-  by Yves Bertot).
diff --git a/doc/changelog/10-standard-library/11686-fix-int-notations.rst b/doc/changelog/10-standard-library/11686-fix-int-notations.rst
deleted file mode 100644
index 4959a9f9b1..0000000000
--- a/doc/changelog/10-standard-library/11686-fix-int-notations.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Changed:**
-  Notations :n:`[|@term|]` and :n:`[||@term||]` for morphisms from 63-bit
-  integers to :g:`Z` and :g:`zn2z int` have been removed in favor of
-  :n:`φ(@term)` and :n:`Φ(@term)` respectively. These notations were
-  breaking Ltac parsing (`#11686 <https://github.com/coq/coq/pull/11686>`_,
-  by Maxime Dénès).
diff --git a/doc/changelog/10-standard-library/11725-cleanup-reals.rst b/doc/changelog/10-standard-library/11725-cleanup-reals.rst
deleted file mode 100644
index 02ee7e6c70..0000000000
--- a/doc/changelog/10-standard-library/11725-cleanup-reals.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Changed:**
-  Use implicit arguments for ``ConstructiveReals``. Move ``ConstructiveReals``
-  into new directory ``Abstract``. Remove imports of implementations inside
-  those ``Abstract`` files. Move implementation by means of Cauchy sequences in new directory ``Cauchy``.
-  (`#11725 <https://github.com/coq/coq/pull/11725>`_,
-  by Vincent Semeria).
diff --git a/doc/changelog/10-standard-library/1185-sort.rst b/doc/changelog/10-standard-library/1185-sort.rst
deleted file mode 100644
index edb5ee3ac4..0000000000
--- a/doc/changelog/10-standard-library/1185-sort.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  The names of ``Sorted_sort`` and ``LocallySorted_sort`` in ``Coq.Sorting.MergeSort``
-  have been swapped to appropriately reflect their meanings
-  (`#1185 <https://github.com/coq/coq/pull/1185>`_,
-  by Lysxia).
diff --git a/doc/changelog/10-standard-library/11880-iter.rst b/doc/changelog/10-standard-library/11880-iter.rst
deleted file mode 100644
index be4e44ce4c..0000000000
--- a/doc/changelog/10-standard-library/11880-iter.rst
+++ /dev/null
@@ -1,8 +0,0 @@
-- **Added:**
-  Facts about ``N.iter`` and ``Pos.iter``:
-
-    - ``N.iter_swap_gen``, ``N.iter_swap``, ``N.iter_succ``, ``N.iter_succ_r``, ``N.iter_add``, ``N.iter_ind``, ``N.iter_invariant``;
-    - ``Pos.iter_succ_r``, ``Pos.iter_ind``.
-
-  (`#11880 <https://github.com/coq/coq/pull/11880>`_,
-  by Lysxia).
diff --git a/doc/changelog/10-standard-library/11891-fix-order-notations.rst b/doc/changelog/10-standard-library/11891-fix-order-notations.rst
deleted file mode 100644
index d58d26244a..0000000000
--- a/doc/changelog/10-standard-library/11891-fix-order-notations.rst
+++ /dev/null
@@ -1,10 +0,0 @@
-- **Changed:**
-  Notations :g:`<=?` and :g:`<?` from ``Coq.Structures.Orders`` and
-  ``Coq.Sorting.Mergesort.NatOrder`` are now at level 70 rather than
-  35, so as to be compatible with the notations defined everywhere
-  else in the standard library.  This may require re-parenthesizing
-  some expressions.  These notations were breaking the ability to
-  import modules from the standard library that were otherwise
-  compatible (fixes `#11890
-  <https://github.com/coq/coq/issues/11890>`_, `#11891
-  <https://github.com/coq/coq/pull/11891>`_, by Jason Gross).
diff --git a/doc/changelog/10-standard-library/11909-fix-≡-level.rst b/doc/changelog/10-standard-library/11909-fix-≡-level.rst
deleted file mode 100644
index 96551be537..0000000000
--- a/doc/changelog/10-standard-library/11909-fix-≡-level.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- **Changed:**
-  The level of :g:`≡` in ``Coq.Numbers.Cyclic.Int63.Int63`` is now 70,
-  no associativity, in line with :g:`=`.  Note that this is a minor
-  incompatibility with developments that declare their own :g:`≡`
-  notation and import ``Int63`` (fixes `#11905
-  <https://github.com/coq/coq/issues/11905>`_, `#11909
-  <https://github.com/coq/coq/pull/11909>`_, by Jason Gross).
diff --git a/doc/changelog/10-standard-library/11946-ollibs-permutation.rst b/doc/changelog/10-standard-library/11946-ollibs-permutation.rst
deleted file mode 100644
index 626677d31a..0000000000
--- a/doc/changelog/10-standard-library/11946-ollibs-permutation.rst
+++ /dev/null
@@ -1,10 +0,0 @@
-- **Added:**
-  Facts about ``Permutation``:
-
-  - structure: ``Permutation_refl'``, ``Permutation_morph_transp``
-  - compatibilities: ``Permutation_app_rot``, ``Permutation_app_swap_app``, ``Permutation_app_middle``, ``Permutation_middle2``, ``Permutation_elt``, ``Permutation_Forall``, ``Permutation_Exists``, ``Permutation_Forall2``, ``Permutation_flat_map``, ``Permutation_list_sum``, ``Permutation_list_max``
-  - inversions: ``Permutation_app_inv_m``, ``Permutation_vs_elt_inv``, ``Permutation_vs_cons_inv``, ``Permutation_vs_cons_cons_inv``, ``Permutation_map_inv``, ``Permutation_image``, ``Permutation_elt_map_inv``
-  - length-preserving definition by means of transpositions ``Permutation_transp`` with associated properties: ``Permutation_transp_sym``, ``Permutation_transp_equiv``, ``Permutation_transp_cons``, ``Permutation_Permutation_transp``, ``Permutation_ind_transp``
-
-  (`#11946 <https://github.com/coq/coq/pull/11946>`_,
-  by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/11957-signotations.rst b/doc/changelog/10-standard-library/11957-signotations.rst
deleted file mode 100644
index fc5d434274..0000000000
--- a/doc/changelog/10-standard-library/11957-signotations.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  notations for sigma types: ``{ x & P & Q }``, ``{ ' pat & P }``, ``{ ' pat & P & Q }``
-  (`#11957 <https://github.com/coq/coq/pull/11957>`_,
-  by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/11992-no-reexports.rst b/doc/changelog/10-standard-library/11992-no-reexports.rst
deleted file mode 100644
index 3f46bfd501..0000000000
--- a/doc/changelog/10-standard-library/11992-no-reexports.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Changed:**
-  No longer re-export ``ListNotations`` from ``Program`` (``Program.Syntax``)
-  (`#11992 <https://github.com/coq/coq/pull/11992>`_,
-  by Antonio Nikishaev).
diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst
deleted file mode 100644
index 42e5eb96eb..0000000000
--- a/doc/changelog/10-standard-library/12008-ollibs-bool.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Added:**
-  Order relations ``lt`` and ``compare`` added in ``Bool.Bool``.
-  Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx``
-  (`#12008 <https://github.com/coq/coq/pull/12008>`_,
-  by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/12014-ollibs-vector.rst b/doc/changelog/10-standard-library/12014-ollibs-vector.rst
deleted file mode 100644
index 87625dd23b..0000000000
--- a/doc/changelog/10-standard-library/12014-ollibs-vector.rst
+++ /dev/null
@@ -1,10 +0,0 @@
-- **Added:**
-  Properties of some operations on vectors:
-
-  - ``nth_order``: ``nth_order_hd``, ``nth_order_tl``, ``nth_order_ext``
-  - ``replace``: ``nth_order_replace_eq``, ``nth_order_replace_neq``, ``replace_id``, ``replace_replace_eq``, ``replace_replace_neq``
-  - ``map``: ``map_id``, ``map_map``, ``map_ext_in``, ``map_ext``
-  - ``Forall`` and ``Forall2``: ``Forall_impl``, ``Forall_forall``, ``Forall_nth_order``, ``Forall2_nth_order``
-
-  (`#12014 <https://github.com/coq/coq/pull/12014>`_,
-  by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/12018-master+implb-characterization.rst b/doc/changelog/10-standard-library/12018-master+implb-characterization.rst
deleted file mode 100644
index 4b0abdfa3b..0000000000
--- a/doc/changelog/10-standard-library/12018-master+implb-characterization.rst
+++ /dev/null
@@ -1,19 +0,0 @@
-- **Added:**
-  Added lemmas
-  :g:`orb_negb_l`,
-  :g:`andb_negb_l`,
-  :g:`implb_true_iff`,
-  :g:`implb_false_iff`,
-  :g:`implb_true_r`,
-  :g:`implb_false_r`,
-  :g:`implb_true_l`,
-  :g:`implb_false_l`,
-  :g:`implb_same`,
-  :g:`implb_contrapositive`,
-  :g:`implb_negb`,
-  :g:`implb_curry`,
-  :g:`implb_andb_distrib_r`,
-  :g:`implb_orb_distrib_r`,
-  :g:`implb_orb_distrib_l` in library :g:`Bool`
-  (`#12018 <https://github.com/coq/coq/pull/12018>`_,`
-  by Hugo Herbelin).`
diff --git a/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst b/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst
deleted file mode 100644
index 95b4cce2f7..0000000000
--- a/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  Definition and properties of cyclic permutations / circular shifts: ``CPermutation``
-  (`#12031 <https://github.com/coq/coq/pull/12031>`_,
-  by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/12044-issue-12015.rst b/doc/changelog/10-standard-library/12044-issue-12015.rst
deleted file mode 100644
index 166fc80fb0..0000000000
--- a/doc/changelog/10-standard-library/12044-issue-12015.rst
+++ /dev/null
@@ -1,10 +0,0 @@
-- **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)).
diff --git a/doc/changelog/10-standard-library/12073-split-nsatz.rst b/doc/changelog/10-standard-library/12073-split-nsatz.rst
deleted file mode 100644
index bc3c24e441..0000000000
--- a/doc/changelog/10-standard-library/12073-split-nsatz.rst
+++ /dev/null
@@ -1,11 +0,0 @@
-- **Changed:**
-  It is now possible to import the :g:`nsatz` machinery without
-  transitively depending on the axioms of the real numbers nor of
-  classical logic by loading ``Coq.nsatz.NsatzTactic`` rather than
-  ``Coq.nsatz.Nsatz``.  Note that some constants have changed kernel
-  names, living in ``Coq.nsatz.NsatzTactic`` rather than
-  ``Coq.nsatz.Nsatz``; this might cause minor incompatibilities that
-  can be fixed by actually running :g:`Import Nsatz` rather than
-  relying on absolute names (fixes `#5445
-  <https://github.com/coq/coq/issues/5445>`_, `#12073
-  <https://github.com/coq/coq/pull/12073>`_, by Jason Gross).
diff --git a/doc/changelog/10-standard-library/12119-issue12119.rst b/doc/changelog/10-standard-library/12119-issue12119.rst
deleted file mode 100644
index 42672b1465..0000000000
--- a/doc/changelog/10-standard-library/12119-issue12119.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:**
-  new lemma ``NoDup_incl_NoDup`` in ``List.v``
-  to remove useless hypothesis `NoDup l'` in ``Sorting.Permutation.NoDup_Permutation_bis``
-  (`#12119 <https://github.com/coq/coq/pull/12119>`_,
-  by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst b/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst
deleted file mode 100644
index f22fff0736..0000000000
--- a/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  :cmd:`Fixpoint`\s of the standard library without a recursive call turned
-  into ordinary :cmd:`Definition`\s
-  (`#12121 <https://github.com/coq/coq/pull/12121>`_,
-  by Hugo Herbelin; fixes `#11903 <https://github.com/coq/coq/pull/11903>`_).
diff --git a/doc/changelog/10-standard-library/12162-bool-leb.rst b/doc/changelog/10-standard-library/12162-bool-leb.rst
deleted file mode 100644
index 6a4070a82e..0000000000
--- a/doc/changelog/10-standard-library/12162-bool-leb.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Deprecated:**
-  ``Bool.leb`` in favor of ``Bool.le``. The definition of ``Bool.le`` is made local to avoid conflicts with ``Nat.le``. As a consequence, previous calls to ``leb`` based on importing ``Bool`` should now be qualified into ``Bool.le`` even if ``Bool`` is imported.
-  (`#12162 <https://github.com/coq/coq/pull/12162>`_,
-  by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst b/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst
deleted file mode 100644
index c80a070181..0000000000
--- a/doc/changelog/10-standard-library/12263-fix-haskell-extraction.rst
+++ /dev/null
@@ -1,9 +0,0 @@
-- **Fixed:**
-  In Haskell extraction with ``ExtrHaskellString``, equality comparisons on
-  strings and characters are now guaranteed to be uniquely well-typed, even in
-  very polymorphic contexts under ``unsafeCoerce``; this is achieved by adding
-  type annotations to the extracted code, and by making ``ExtrHaskellString``
-  export ``ExtrHaskellBasic`` (`#12263
-  <https://github.com/coq/coq/pull/12263>`_, fixes `#12257
-  <https://github.com/coq/coq/issues/12257>`_ and `#12258
-  <https://github.com/coq/coq/issues/12258>`_, by Jason Gross).
diff --git a/doc/changelog/10-standard-library/12287-zero-of-Q.rst b/doc/changelog/10-standard-library/12287-zero-of-Q.rst
deleted file mode 100644
index ba2c74379b..0000000000
--- a/doc/changelog/10-standard-library/12287-zero-of-Q.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Changed:**
-  Replace `CRzero` and `CRone` by `CR_of_Q 0` and `CR_of_Q 1` in `ConstructiveReals`
-  (`#12287 <https://github.com/coq/coq/pull/12287>`_,
-  by Vincent Semeria).
diff --git a/doc/changelog/10-standard-library/12288-constructive-experimental.rst b/doc/changelog/10-standard-library/12288-constructive-experimental.rst
deleted file mode 100644
index ec9b66bd7a..0000000000
--- a/doc/changelog/10-standard-library/12288-constructive-experimental.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- **Changed:**
-  Split files `ConstructiveMinMax` and `ConstructivePower`.
-
-  .. warning:: The constructive reals modules are marked as experimental.
-
-  (`#12288 <https://github.com/coq/coq/pull/12288>`_,
-  by Vincent Semeria).
diff --git a/doc/changelog/10-standard-library/9803-reals.rst b/doc/changelog/10-standard-library/9803-reals.rst
deleted file mode 100644
index 86c5e45bc1..0000000000
--- a/doc/changelog/10-standard-library/9803-reals.rst
+++ /dev/null
@@ -1,14 +0,0 @@
-- **Changed:**
-  Cleanup of names in the Reals theory: replaced `tan_is_inj` with `tan_inj` and replaced `atan_right_inv` with `tan_atan` -
-  compatibility notations are provided. Moved various auxiliary lemmas from `Ratan.v` to more appropriate places.
-  (`#9803 <https://github.com/coq/coq/pull/9803>`_,
-  by Laurent Théry and Michael Soegtrop).
-
-- **Added:** to the Reals theory:
-  inverse trigonometric functions `asin` and `acos` with lemmas for the derivatives, bounds and special values of these functions;
-  an extensive set of identities between trigonometric functions and their inverse functions;
-  lemmas for the injectivity of sine and cosine;
-  lemmas on the derivative of the inverse of decreasing functions and on the derivative of horizontally mirrored functions;
-  various generic auxiliary lemmas and definitions for Rsqr, sqrt, posreal an others.
-  (`#9803 <https://github.com/coq/coq/pull/9803>`_,
-  by Laurent Théry and Michael Soegtrop).
diff --git a/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst b/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst
deleted file mode 100644
index dc76178e0d..0000000000
--- a/doc/changelog/11-infrastructure-and-dependencies/11245-bye+py2.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Removed:**
-  Python 2 is not longer required in any part of the codebase
-  (`#11245 <https://github.com/coq/coq/pull/11245>`_,
-  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst b/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst
deleted file mode 100644
index 35a618ea8d..0000000000
--- a/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst
+++ /dev/null
@@ -1,6 +0,0 @@
-- **Changed:**
-  Minimal versions of dependencies for building the reference manual:
-  now requires Sphinx 2.3.1+, sphinx_rtd_theme 0.4.3+ and
-  sphinxcontrib-bibtex 0.4.2+
-  (`#12224 <https://github.com/coq/coq/pull/12224>`_,
-  by Jim Fehrle and Théo Zimmermann).
diff --git a/doc/changelog/12-misc/10486-native-string-extraction.rst b/doc/changelog/12-misc/10486-native-string-extraction.rst
deleted file mode 100644
index 0636e303c4..0000000000
--- a/doc/changelog/12-misc/10486-native-string-extraction.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- **Added:**
-  Support for better extraction of strings in OCaml and Haskell:
-  `ExtOcamlNativeString` provides bindings from the Coq `String` type to
-  the OCaml `string` type, and string literals can be extracted to literals,
-  both in OCaml and Haskell (`#10486
-  <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from
-  Maxime Dénès, review by Hugo Herbelin).
diff --git a/doc/changelog/12-misc/11755-exn+tclfail.rst b/doc/changelog/12-misc/11755-exn+tclfail.rst
deleted file mode 100644
index 800cc09e01..0000000000
--- a/doc/changelog/12-misc/11755-exn+tclfail.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Added:**
-  Backtrace information for tactics has been improved
-  (`#11755 <https://github.com/coq/coq/pull/11755>`_,
-  by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 363148e2a0..6a9176cbfa 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -8,6 +8,887 @@ Recent changes
 
    .. include:: ../unreleased.rst
 
+Version 8.12
+------------
+
+Summary of changes
+~~~~~~~~~~~~~~~~~~
+
+Changes in 8.12+beta1
+~~~~~~~~~~~~~~~~~~~~~
+
+**Specification language, type inference**
+
+- **Changed:**
+  The deprecation warning raised since Coq 8.10 when a trailing
+  implicit is declared to be non-maximally inserted (with the command
+  :cmd:`Arguments`) has been turned into an error
+  (`#11368 <https://github.com/coq/coq/pull/11368>`_,
+  by SimonBoulier).
+- **Added:**
+  Warn when manual implicit arguments are used in unexpected positions
+  of a term (e.g. in `Check id (forall {x}, x)`) or when an implicit
+  argument name is shadowed (e.g. in `Check fun f : forall {x:nat}
+  {x}, nat => f`)
+  (`#10202 <https://github.com/coq/coq/pull/10202>`_,
+  by Hugo Herbelin).
+- **Added:**
+  :cmd:`Arguments` now supports setting
+  implicit an anonymous argument, as e.g. in `Arguments id {A} {_}`
+  (`#11098 <https://github.com/coq/coq/pull/11098>`_,
+  by Hugo Herbelin, fixes `#4696
+  <https://github.com/coq/coq/pull/4696>`_, `#5173
+  <https://github.com/coq/coq/pull/5173>`_, `#9098
+  <https://github.com/coq/coq/pull/9098>`_).
+- **Added:**
+  Syntax for non-maximal implicit arguments in definitions and terms using
+  square brackets. The syntax is ``[x : A]``, ``[x]``, ```[A]``
+  to be consistent with the command :cmd:`Arguments`
+  (`#11235 <https://github.com/coq/coq/pull/11235>`_,
+  by SimonBoulier).
+- **Added:**
+  :cmd:`Implicit Types` are now taken into account for printing. To inhibit it,
+  unset the :flag:`Printing Use Implicit Types` flag
+  (`#11261 <https://github.com/coq/coq/pull/11261>`_,
+  by Hugo Herbelin, granting `#10366 <https://github.com/coq/coq/pull/10366>`_).
+- **Added:**
+  New syntax :cmd:`Inductive` :n:`@ident {* @binder } | {* @binder } := ...`
+  to specify which parameters of an inductive type are uniform.
+  See :ref:`parametrized-inductive-types`
+  (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert).
+- **Added:**
+  Warn when using :cmd:`Fixpoint` or :cmd:`CoFixpoint` for
+  definitions which are not recursive
+  (`#12121 <https://github.com/coq/coq/pull/12121>`_,
+  by Hugo Herbelin).
+- **Fixed:**
+  More robust and expressive treatment of implicit inductive
+  parameters in inductive declarations (`#11579
+  <https://github.com/coq/coq/pull/11579>`_, by Maxime Dénès, Gaëtan
+  Gilbert and Jasper Hugunin; fixes `#7253
+  <https://github.com/coq/coq/pull/7253>`_ and `#11585
+  <https://github.com/coq/coq/pull/11585>`_).
+- **Fixed:**
+  Anomaly which could be raised when printing binders with implicit types
+  (`#12323 <https://github.com/coq/coq/pull/12323>`_,
+  by Hugo Herbelin; fixes `#12322 <https://github.com/coq/coq/pull/12322>`_).
+
+**Notations**
+
+- **Changed:** Notation scopes are now always inherited in
+  notations binding a partially applied constant, including for
+  notations binding an expression of the form :n:`@@qualid`. The latter was
+  not the case beforehand
+  (part of `#11120 <https://github.com/coq/coq/pull/11120>`_).
+- **Changed:**
+  The printing algorithm now interleaves search for notations and removal of coercions
+  (`#11172 <https://github.com/coq/coq/pull/11172>`_, by Hugo Herbelin).
+- **Changed:**
+  Nicer printing for decimal constants in R and Q.
+  1.5 is now printed 1.5 rather than 15e-1
+  (`#11848 <https://github.com/coq/coq/pull/11848>`_,
+  by Pierre Roux).
+- **Removed:** deprecated ``compat`` modifier of :cmd:`Notation`
+  and :cmd:`Infix` commands. Use the :attr:`deprecated` attribute instead
+  (`#11113 <https://github.com/coq/coq/pull/11113>`_,
+  by Théo Zimmermann, with help from Jason Gross).
+- **Deprecated:**
+  Numeral Notation on ``Decimal.uint``, ``Decimal.int`` and
+  ``Decimal.decimal`` are replaced respectively by numeral notations
+  on ``Numeral.uint``, ``Numeral.int`` and ``Numeral.numeral``
+  (`#11948 <https://github.com/coq/coq/pull/11948>`_,
+  by Pierre Roux).
+- **Added:**
+  Notations declared with the ``where`` clause in the declaration of
+  inductive types, coinductive types, record fields, fixpoints and
+  cofixpoints now support the ``only parsing`` modifier
+  (`#11602 <https://github.com/coq/coq/pull/11602>`_,
+  by Hugo Herbelin).
+- **Added:**
+  :flag:`Printing Parentheses` flag to print parentheses even when
+  implied by associativity or precedence
+  (`#11650 <https://github.com/coq/coq/pull/11650>`_,
+  by Hugo Herbelin and Abhishek Anand).
+- **Added:**
+  Numeral notations now parse hexadecimal constants such as ``0x2a``
+  or ``0xb.2ap-2``. Parsers added for :g:`nat`, :g:`positive`, :g:`Z`,
+  :g:`N`, :g:`Q`, :g:`R`, primitive integers and primitive floats
+  (`#11948 <https://github.com/coq/coq/pull/11948>`_,
+  by Pierre Roux).
+- **Added:**
+  Abbreviations support arguments occurring both in term and binder position
+  (`#8808 <https://github.com/coq/coq/pull/8808>`_,
+  by Hugo Herbelin).
+- **Fixed:**
+  Different interpretations in different scopes of the same notation
+  string can now be associated to different printing formats (`#10832
+  <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin,
+  fixes `#6092 <https://github.com/coq/coq/issues/6092>`_
+  and `#7766 <https://github.com/coq/coq/issues/7766>`_).
+- **Fixed:** Parsing and printing consistently handle inheritance of implicit
+  arguments in notations. With the exception of notations of
+  the form :n:`Notation @string := @@qualid` and :n:`Notation @ident := @@qualid` which
+  inhibit implicit arguments, all notations binding a partially
+  applied constant, as e.g. in :n:`Notation @string := (@qualid {+ @arg })`,
+  or :n:`Notation @string := (@@qualid {+ @arg })`, or
+  :n:`Notation @ident := (@qualid {+ @arg })`, or :n:`Notation @ident
+  := (@@qualid {+ @arg })`, inherit the remaining implicit arguments
+  (`#11120 <https://github.com/coq/coq/pull/11120>`_, by Hugo
+  Herbelin, fixing `#4690 <https://github.com/coq/coq/pull/4690>`_ and
+  `#11091 <https://github.com/coq/coq/pull/11091>`_).
+- **Fixed:**
+  Notations in ``only printing`` mode do not uselessly reserve parsing keywords
+  (`#11590 <https://github.com/coq/coq/pull/11590>`_,
+  by Hugo Herbelin, fixes `#9741 <https://github.com/coq/coq/pull/9741>`_).
+- **Fixed:**
+  Numeral Notations now play better with multiple scopes for the same
+  inductive type. Previously, when multiple numeral notations were defined
+  for the same inductive, only the last one was considered for
+  printing. Now, among the notations that are usable for printing and either
+  have a scope delimiter or are open, the selection is made according
+  to the order of open scopes, or according to the last defined
+  notation if no appropriate scope is open
+  (`#12163 <https://github.com/coq/coq/pull/12163>`_,
+  fixes `#12159 <https://github.com/coq/coq/pull/12159>`_,
+  by Pierre Roux, review by Hugo Herbelin and Jason Gross).
+
+**Tactics**
+
+- **Changed:**
+  The :tacn:`rapply` tactic in :g:`Coq.Program.Tactics` now handles
+  arbitrary numbers of underscores and takes in a :g:`uconstr`.  In
+  rare cases where users were relying on :tacn:`rapply` inserting
+  exactly 15 underscores and no more, due to the lemma having a
+  completely unspecified codomain (and thus allowing for any number of
+  underscores), the tactic will now loop instead (`#10760
+  <https://github.com/coq/coq/pull/10760>`_, by Jason Gross).
+- **Changed:**
+  The :g:`auto with zarith` tactic and variations (including
+  :tacn:`intuition`) may now call :tacn:`lia` instead of :tacn:`omega`
+  (when the `Omega` module is loaded); more goals may be automatically
+  solved, fewer section variables will be captured spuriously
+  (`#11018 <https://github.com/coq/coq/pull/11018>`_,
+  by Vincent Laporte).
+- **Changed:**
+  The new :flag:`NativeCompute Timing` flag causes calls to
+  :tacn:`native_compute` (as well as kernel calls to the native
+  compiler) to emit separate timing information about conversion to
+  native code, compilation, execution, and reification.  It replaces
+  the timing information previously emitted when the `-debug`
+  command-line flag was set, and allows more fine-grained timing of
+  the native compiler
+  (`#11025 <https://github.com/coq/coq/pull/11025>`_, by Jason Gross).
+  Additionally, the timing information now uses real time rather than
+  user time (fixes `#11962
+  <https://github.com/coq/coq/issues/11962>`_, `#11963
+  <https://github.com/coq/coq/pull/11963>`_, by Jason Gross)
+- **Changed:**
+  Improve the efficiency of `PreOmega.elim_let` using an iterator implemented in OCaml
+  (`#11370 <https://github.com/coq/coq/pull/11370>`_, by Frédéric Besson).
+- **Changed:**
+  Improve the efficiency of :tacn:`zify` by rewritting the remaining Ltac code in OCaml
+  (`#11429 <https://github.com/coq/coq/pull/11429>`_, by Frédéric Besson).
+- **Changed:**
+  The default tactic used by :g:`firstorder` is
+  :g:`auto with core` instead of :g:`auto with *`;
+  see :ref:`decisionprocedures` for details;
+  old behavior can be reset by using the `-compat 8.12` command-line flag;
+  to ease the migration of legacy code, the default solver can be set to `debug auto with *`
+  with `Set Firstorder Solver debug auto with *`
+  (`#11760 <https://github.com/coq/coq/pull/11760>`_,
+  by Vincent Laporte).
+- **Changed:**
+  :tacn:`autounfold` no longer fails when the :cmd:`Opaque`
+  command is used on constants in the hint databases
+  (`#11883 <https://github.com/coq/coq/pull/11883>`_,
+  by Attila Gáspár).
+- **Changed:**
+  Tactics with qualified name of the form ``Coq.Init.Notations`` are
+  now qualified with prefix ``Coq.Init.Ltac``; users of the ``-noinit``
+  option should now import ``Coq.Init.Ltac`` if they want to use Ltac
+  (`#12023 <https://github.com/coq/coq/pull/12023>`_,
+  by Hugo Herbelin; minor source of incompatibilities).
+- **Changed:**
+  Tactic :tacn:`subst` :n:`@ident` now fails over a section variable which is
+  indirectly dependent in the goal; the incompatibility can generally
+  be fixed by first clearing the hypotheses causing an indirect
+  dependency, as reported by the error message, or by using :tacn:`rewrite` :n:`... in *`
+  instead; similarly, :tacn:`subst` has no more effect on such variables
+  (`#12146 <https://github.com/coq/coq/pull/12146>`_,
+  by Hugo Herbelin; fixes `#10812 <https://github.com/coq/coq/pull/10812>`_
+  and `#12139 <https://github.com/coq/coq/pull/12139>`_).
+- **Changed:**
+  The check that :tacn:`unfold` arguments were indeed unfoldable has been moved to runtime
+  (`#12256 <https://github.com/coq/coq/pull/12256>`_,
+  by Pierre-Marie Pédrot; fixes
+  `#5764 <https://github.com/coq/coq/issues/5764>`_,
+  `#5159 <https://github.com/coq/coq/issues/5159>`_,
+  `#4925 <https://github.com/coq/coq/issues/4925>`_
+  and `#11727 <https://github.com/coq/coq/issues/11727>`_).
+- **Changed**
+  When the tactic :tacn:`functional induction` :n:`c__1 c__2 ... c__n` is used
+  with no parenthesis around :n:`c__1 c__2 ... c__n`, :n:`c__1 c__2 ... c__n` is now
+  read as one single applicative term. In particular implicit
+  arguments should be omitted. Rare source of incompatibility
+  (`#12326 <https://github.com/coq/coq/pull/12326>`_,
+  by Pierre Courtieu).
+- **Removed:**
+  Undocumented ``omega with``.  Using :tacn:`lia` is the recommended
+  replacement, although the old semantics of ``omega with *`` can also
+  be recovered with ``zify; omega``
+  (`#11288 <https://github.com/coq/coq/pull/11288>`_,
+  by Emilio Jesus Gallego Arias).
+- **Removed:**
+  Deprecated syntax `_eqn` for :tacn:`destruct` and :tacn:`remember`.
+  Use `eqn:` syntax instead
+  (`#11877 <https://github.com/coq/coq/pull/11877>`_,
+  by Hugo Herbelin).
+- **Removed:**
+  `at` clauses can no longer be used with :tacn:`autounfold`.
+  Since they had no effect, it is safe to remove them
+  (`#11883 <https://github.com/coq/coq/pull/11883>`_,
+  by Attila Gáspár).
+- **Deprecated:**
+  The :tacn:`omega` tactic is deprecated;
+  use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead
+  (`#11976 <https://github.com/coq/coq/pull/11976>`_,
+  by Vincent Laporte).
+- **Added:**
+  The :tacn:`zify` tactic is now aware of `Pos.pred_double`, `Pos.pred_N`,
+  `Pos.of_nat`, `Pos.add_carry`, `Pos.pow`, `Pos.square`, `Z.pow`, `Z.double`,
+  `Z.pred_double`, `Z.succ_double`, `Z.square`, `Z.div2`, and `Z.quot2`.
+  Injections for internal definitions in module `ZifyBool` (`isZero` and `isLeZero`)
+  are also added to help users to declare new :tacn:`zify` class instances using
+  Micromega tactics
+  (`#10998 <https://github.com/coq/coq/pull/10998>`_, by Kazuhiko Sakaguchi).
+- **Added:**
+  :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls
+  (`#11474 <https://github.com/coq/coq/pull/11474>`_,  by Frédéric Besson).
+- **Added:**
+  Syntax :tacn:`pose proof` :n:`(@ident:=@term)` as an alternative to
+  :tacn:`pose proof` :n:`@term as @ident`, following the model of
+  :tacn:`pose` :n:`(@ident:=@term)`
+  (`#11522 <https://github.com/coq/coq/pull/11522>`_,
+  by Hugo Herbelin).
+- **Added:**
+  New tactical :tacn:`with_strategy` which behaves like the command
+  :cmd:`Strategy`, with effects local to the given tactic
+  (`#12129 <https://github.com/coq/coq/pull/12129>`_, by Jason Gross).
+- **Added:**
+  The :tacn:`zify` tactic is now aware of `Nat.le`, `Nat.lt` and `Nat.eq`
+  (`#12213 <https://github.com/coq/coq/pull/12213>`_, by Frédéric Besson;
+  fixes `#12210 <https://github.com/coq/coq/issues/12210>`_).
+- **Fixed:**
+  :tacn:`zify` now handles :g:`Z.pow_pos` by default.
+  In Coq 8.11, this was the case only when loading module
+  :g:`ZifyPow` because this triggered a regression of :tacn:`lia`.
+  The regression is now fixed, and the module kept only for compatibility
+  (`#11362 <https://github.com/coq/coq/pull/11362>`_,
+  fixes `#11191 <https://github.com/coq/coq/issues/11191>`_,
+  by Frédéric Besson).
+- **Fixed:**
+  Efficiency regression of :tacn:`lia`
+  (`#11474 <https://github.com/coq/coq/pull/11474>`_,
+  fixes `#11436 <https://github.com/coq/coq/issues/11436>`_,
+  by Frédéric Besson).
+- **Fixed:**
+  The behavior of :tacn:`autounfold` no longer depends on the names of terms and modules
+  (`#11883 <https://github.com/coq/coq/pull/11883>`_,
+  fixes `#7812 <https://github.com/coq/coq/issues/7812>`_,
+  by Attila Gáspár).
+- **Fixed:**
+  Wrong type error in tactic :tacn:`functional induction`
+  (`#12326 <https://github.com/coq/coq/pull/12326>`_,
+  by Pierre Courtieu,
+  fixes `#11761 <https://github.com/coq/coq/issues/11761>`_,
+  reported by Lasse Blaauwbroek).
+
+**Tactic language**
+
+- **Changed:**
+  The "reference" tactic generic argument now accepts arbitrary
+  variables of the goal context
+  (`#12254 <https://github.com/coq/coq/pull/12254>`_,
+  by Pierre-Marie Pédrot).
+- **Added:**
+  An array library for Ltac2 (as compatible as possible with OCaml standard library)
+  (`#10343 <https://github.com/coq/coq/pull/10343>`_,
+  by Michael Soegtrop).
+- **Added:**
+  The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to
+  give a name to the old value so as to be able to reuse it inside the
+  new one
+  (`#11503 <https://github.com/coq/coq/pull/11503>`_,
+  by Pierre-Marie Pédrot).
+- **Added:**
+  Ltac2 notations for :tacn:`enough` and :tacn:`eenough`
+  (`#11740 <https://github.com/coq/coq/pull/11740>`_,
+  by Michael Soegtrop).
+- **Added:**
+  New Ltac2 function ``Fresh.Free.of_goal`` to return the list of
+  names of declarations of the current goal; new Ltac2 function
+  ``Fresh.in_goal`` to return a variable fresh in the current goal
+  (`#11882 <https://github.com/coq/coq/pull/11882>`_,
+  by Hugo Herbelin).
+- **Added:**
+  Ltac2 notations for reductions in terms: :n:`eval @red_expr in @ltac2_term`
+  (`#11981 <https://github.com/coq/coq/pull/11981>`_,
+  by Michael Soegtrop).
+- **Fixed:**
+  The :flag:`Ltac Profiling` machinery now correctly handles
+  backtracking into multi-success tactics.  The call-counts of some
+  tactics are unfortunately inflated by 1, as some tactics are
+  implicitly implemented as :g:`tac + fail`, which has two
+  entry-points rather than one (fixes `#12196
+  <https://github.com/coq/coq/issues/12196>`_, `#12197
+  <https://github.com/coq/coq/pull/12197>`_, by Jason Gross).
+
+**SSReflect**
+
+- **Changed:** The :cmd:`Search (ssreflect)` command that used to be
+  available when loading the `ssreflect` plugin has been moved to a
+  separate plugin that needs to be loaded separately: `ssrsearch`
+  (part of `#8855 <https://github.com/coq/coq/pull/8855>`_, fixes
+  `#12253 <https://github.com/coq/coq/issues/12253>`_, by Théo
+  Zimmermann).
+- **Deprecated:** :cmd:`Search (ssreflect)` (available through
+  `Require ssrsearch.`) in favor of the `headconcl:` clause of
+  :cmd:`Search` (part of `#8855
+  <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann).
+
+**Flags, options and attributes**
+
+- **Changed:** :term:`Legacy attributes <attribute>` can now be passed
+  in any order (`#11665 <https://github.com/coq/coq/pull/11665>`_, by
+  Théo Zimmermann).
+- **Removed:** ``Typeclasses Axioms Are Instances`` flag, deprecated since 8.10.
+  Use :cmd:`Declare Instance` for axioms which should be instances
+  (`#11185 <https://github.com/coq/coq/pull/11185>`_, by Théo Zimmermann).
+- **Removed:** Deprecated unsound compatibility ``Template Check``
+  flag that was introduced in 8.10 to help users gradually move their
+  template polymorphic inductive type definitions outside sections
+  (`#11546 <https://github.com/coq/coq/pull/11546>`_, by Pierre-Marie
+  Pédrot).
+- **Removed:**
+  Deprecated ``Shrink Obligations`` flag
+  (`#11828 <https://github.com/coq/coq/pull/11828>`_,
+  by Emilio Jesus Gallego Arias).
+- **Removed:**
+  Unqualified ``polymorphic``, ``monomorphic``, ``template``,
+  ``notemplate`` attributes (they were deprecated since Coq 8.10).
+  Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`,
+  :attr:`universes(template)` and :attr:`universes(notemplate)` instead
+  (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann).
+- **Deprecated:**
+  :flag:`Hide Obligations` flag
+  (`#11828 <https://github.com/coq/coq/pull/11828>`_,
+  by Emilio Jesus Gallego Arias).
+- **Added:** Handle the :attr:`local` attribute in :cmd:`Canonical
+  Structure` declarations (`#11162
+  <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi).
+- **Added:**
+  New attributes supported when defining an inductive type
+  :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and
+  :attr:`private(matching)`, which correspond to legacy attributes
+  ``Cumulative``, ``NonCumulative``, and the previously undocumented
+  ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by
+  Théo Zimmermann).
+- **Added:**
+  The :cmd:`Hint` commands now accept the :attr:`export` locality as
+  an attribute, allowing to make import-scoped hints
+  (`#11812 <https://github.com/coq/coq/pull/11812>`_,
+  by Pierre-Marie Pédrot).
+- **Added:**
+  :flag:`Cumulative StrictProp` to control cumulativity of |SProp|
+  (`#12034 <https://github.com/coq/coq/pull/12034>`_, by Gaëtan
+  Gilbert).
+
+**Commands**
+
+- **Changed:**
+  The :cmd:`Coercion` command has been improved to check the coherence of the
+  inheritance graph. It checks whether a circular inheritance path of `C >-> C`
+  is convertible with the identity function or not, then report it as an
+  ambiguous path if it is not.  The new mechanism does not report ambiguous
+  paths that are redundant with others. For example, checking the ambiguity of
+  `[f; g]` and `[f'; g]` is redundant with that of `[f]` and `[f']` thus will
+  not be reported
+  (`#11258 <https://github.com/coq/coq/pull/11258>`_,
+  by Kazuhiko Sakaguchi).
+- **Changed:**
+  Several commands (:cmd:`Search`, :cmd:`About`, ...) now print the
+  implicit arguments in brackets when printing types (`#11795
+  <https://github.com/coq/coq/pull/11795>`_, by Simon Boulier).
+- **Changed:**
+  :cmd:`Redirect` now obeys the :opt:`Printing Width` and
+  :opt:`Printing Depth` options
+  (`#12358 <https://github.com/coq/coq/pull/12358>`_,
+  by Emilio Jesus Gallego Arias).
+- **Removed:**
+  Recursive OCaml loadpaths are not supported anymore; the command
+  ``Add Rec ML Path`` has been removed; :cmd:`Add ML Path` is now the
+  preferred one. We have also dropped support for the non-qualified
+  version of the :cmd:`Add LoadPath` command, that is to say,
+  the ``Add LoadPath dir`` version; now,
+  you must always specify a prefix now using ``Add Loadpath dir as Prefix``
+  (`#11618 <https://github.com/coq/coq/pull/11618>`_,
+  by Emilio Jesus Gallego Arias).
+- **Removed:** undocumented ``Chapter`` command.  Use :cmd:`Section`
+  instead (`#11746 <https://github.com/coq/coq/pull/11746>`_, by Théo
+  Zimmermann).
+- **Removed:** ``SearchAbout`` command that was deprecated since 8.5.
+  Use :cmd:`Search` instead
+  (`#11944 <https://github.com/coq/coq/pull/11944>`_, by Jim Fehrle).
+- **Deprecated:**
+  Declaration of arbitrary terms as hints. Global references are now
+  preferred (`#7791 <https://github.com/coq/coq/pull/7791>`_, by
+  Pierre-Marie Pédrot).
+- **Deprecated:** :cmd:`SearchHead` in favor of the new `headconcl:`
+  clause of :cmd:`Search` (part of `#8855
+  <https://github.com/coq/coq/pull/8855>`_, by Théo Zimmermann).
+- **Added:**
+  :cmd:`Print Canonical Projections` can now take constants as
+  arguments and prints only the unification rules that involve or are
+  synthesized from the given constants (`#10747
+  <https://github.com/coq/coq/pull/10747>`_, by Kazuhiko Sakaguchi).
+- **Added:** A section variable introduced with :cmd:`Let` can be
+  declared as a :cmd:`Canonical Structure` (`#11164
+  <https://github.com/coq/coq/pull/11164>`_, by Enrico Tassi).
+- **Added:** Support for universe bindings and universe contrainsts in
+  :cmd:`Let` definitions (`#11534
+  <https://github.com/coq/coq/pull/11534>`_, by Théo Zimmermann).
+- **Added:** Support for new clauses `hyp:`, `headhyp:`, `concl:`,
+  `headconcl:`, `head:` and `is:` in :cmd:`Search`.  Support for
+  complex search queries combining disjunctions, conjunctions and
+  negations (`#8855 <https://github.com/coq/coq/pull/8855>`_, by Hugo
+  Herbelin, with ideas from Cyril Cohen and help from Théo
+  Zimmermann).
+- **Fixed:**
+  A printing bug in the presence of elimination principles with local definitions
+  (`#12295 <https://github.com/coq/coq/pull/12295>`_,
+  by Hugo Herbelin; fixes `#12233 <https://github.com/coq/coq/pull/12233>`_).
+- **Fixed:**
+  Anomalies with :cmd:`Show Proof`
+  (`#12296 <https://github.com/coq/coq/pull/12296>`_,
+  by Hugo Herbelin; fixes
+  `#12234 <https://github.com/coq/coq/pull/12234>`_).
+
+**Tools**
+
+- **Changed:**
+  Internal options and behavior of ``coqdep``. ``coqdep``
+  no longer works as a replacement for ``ocamldep``, thus ``.ml``
+  files are not supported as input. Also, several deprecated options
+  have been removed: ``-w``, ``-D``, ``-mldep``, ``-prefix``,
+  ``-slash``, and ``-dumpbox``. Passing ``-boot`` to ``coqdep`` will
+  not load any path by default now, ``-R/-Q`` should be used instead
+  (`#11523 <https://github.com/coq/coq/pull/11523>`_ and
+  `#11589 <https://github.com/coq/coq/pull/11589>`_,
+  by Emilio Jesus Gallego Arias).
+- **Changed:**
+  The order in which the require flags `-ri`, `-re`, `-rfrom`, etc.
+  and the option flags `-set`, `-unset` are given now matters.  In
+  particular, it is now possible to interleave the loading of plugins
+  and the setting of options by choosing the right order for these
+  flags.  The load flags `-l` and `-lv` are still processed afterward
+  for now (`#11851 <https://github.com/coq/coq/pull/11851>`_ and
+  `#12097 <https://github.com/coq/coq/pull/12097>`_,
+  by Lasse Blaauwbroek).
+- **Changed:**
+  The ``cleanall`` target of a makefile generated by ``coq_makefile``
+  now erases ``.lia.cache`` and ``.nia.cache`` (`#12006
+  <https://github.com/coq/coq/pull/12006>`_, by Olivier Laurent).
+- **Changed:**
+  The output of ``make TIMED=1`` (and therefore the timing targets
+  such as ``print-pretty-timed`` and ``print-pretty-timed-diff``) now
+  displays the full name of the output file being built, rather than
+  the stem of the rule (which was usually the filename without the
+  extension, but in general could be anything for user-defined rules
+  involving ``%``) (`#12126
+  <https://github.com/coq/coq/pull/12126>`_, by Jason Gross).
+- **Changed:**
+  When passing ``TIMED=1`` to ``make`` with either Coq's own makefile
+  or a ``coq_makefile``\-made makefile, timing information is now
+  printed for OCaml files as well (`#12211
+  <https://github.com/coq/coq/pull/12211>`_, by Jason Gross).
+- **Changed:**
+  The pretty-timed scripts and targets now print a newline at the end of their
+  tables, rather than creating text with no trailing newline (`#12368
+  <https://github.com/coq/coq/pull/12368>`_, by Jason Gross).
+- **Removed:**
+  The `-load-ml-source` and `-load-ml-object` command-line options
+  have been removed; their use was very limited, you can achieve the same adding
+  additional object files in the linking step or using a plugin
+  (`#11409 <https://github.com/coq/coq/pull/11409>`_, by Emilio Jesus Gallego Arias).
+- **Removed:**
+  The confusingly-named `-require` command-line option, which was
+  deprecated since 8.11.  Use the equivalent `-require-import` / `-ri`
+  options instead
+  (`#12005 <https://github.com/coq/coq/pull/12005>`_,
+  by Théo Zimmermann).
+- **Deprecated:**
+  ``-cumulative-sprop`` command-line flag in favor of the new
+  :flag:`Cumulative StrictProp` flag (`#12034
+  <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert).
+- **Added:**
+  A new documentation environment ``details`` to make certain portion
+  of a Coq document foldable.  See :ref:`coqdoc-hide-show`
+  (`#10592 <https://github.com/coq/coq/pull/10592>`_,
+  by Thomas Letan).
+- **Added:**
+  The ``make-both-single-timing-files.py`` script now accepts a
+  ``--fuzz=N`` parameter on the command line which determines how many
+  characters two lines may be offset in the "before" and "after"
+  timing logs while still being considered the same line.  When
+  invoking this script via the ``print-pretty-single-time-diff``
+  target in a ``Makefile`` made by ``coq_makefile``, you can set this
+  argument by passing ``TIMING_FUZZ=N`` to ``make`` (`#11302
+  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
+- **Added:**
+  The ``make-one-time-file.py`` and ``make-both-time-files.py``
+  scripts now accept a ``--real`` parameter on the command line to
+  print real times rather than user times in the tables.  The
+  ``make-both-single-timing-files.py`` script accepts a ``--user``
+  parameter to use user times.  When invoking these scripts via the
+  ``print-pretty-timed`` or ``print-pretty-timed-diff`` or
+  ``print-pretty-single-time-diff`` targets in a ``Makefile`` made by
+  ``coq_makefile``, you can set this argument by passing
+  ``TIMING_REAL=1`` (to pass ``--real``) or ``TIMING_REAL=0`` (to pass
+  ``--user``) to ``make`` (`#11302
+  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
+- **Added:**
+  Coq's build system now supports both ``TIMING_FUZZ``,
+  ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile``
+  made by ``coq_makefile`` (`#11302
+  <https://github.com/coq/coq/pull/11302>`_, by Jason Gross).
+- **Added:**
+  The ``make-one-time-file.py`` and ``make-both-time-files.py``
+  scripts now include peak memory usage information in the tables (can
+  be turned off by the ``--no-include-mem`` command-line parameter),
+  and a ``--sort-by-mem`` parameter to sort the tables by memory
+  rather than time.  When invoking these scripts via the
+  ``print-pretty-timed`` or ``print-pretty-timed-diff`` targets in a
+  ``Makefile`` made by ``coq_makefile``, you can set this argument by
+  passing ``TIMING_INCLUDE_MEM=0`` (to pass ``--no-include-mem``) and
+  ``TIMING_SORT_BY_MEM=1`` (to pass ``--sort-by-mem``) to ``make``
+  (`#11606 <https://github.com/coq/coq/pull/11606>`_, by Jason Gross).
+- **Added:**
+  Coq's build system now supports both ``TIMING_INCLUDE_MEM`` and
+  ``TIMING_SORT_BY_MEM`` just like a ``Makefile`` made by
+  ``coq_makefile`` (`#11606 <https://github.com/coq/coq/pull/11606>`_,
+  by Jason Gross).
+- **Added:**
+  New ``coqc`` / ``coqtop`` option ``-boot`` that will not bind the
+  `Coq` library prefix by default
+  (`#11617 <https://github.com/coq/coq/pull/11617>`_,
+  by Emilio Jesus Gallego Arias).
+- **Added:**
+  Definitions in coqdoc link to themselves, giving access in html to their own url
+  (`#12026 <https://github.com/coq/coq/pull/12026>`_,
+  by Hugo Herbelin; granting `#7093 <https://github.com/coq/coq/pull/7093>`_).
+- **Added:**
+  Hyperlinks on bound variables in coqdoc
+  (`#12033 <https://github.com/coq/coq/pull/12033>`_,
+  by Hugo Herbelin; it incidentally fixes
+  `#7697 <https://github.com/coq/coq/pull/7697>`_).
+- **Added:**
+  Highlighting of link targets in coqdoc
+  (`#12091 <https://github.com/coq/coq/pull/12091>`_,
+  by Hugo Herbelin).
+- **Fixed:**
+  The various timing targets for Coq's standard library now correctly
+  display and label the "before" and "after" columns, rather than
+  mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_
+  fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason
+  Gross).
+- **Fixed:**
+  The sorting order of the timing script ``make-both-time-files.py``
+  and the target ``print-pretty-timed-diff`` is now deterministic even
+  when the sorting order is ``absolute`` or ``diff``; previously the
+  relative ordering of two files with identical times was
+  non-deterministic (`#11606
+  <https://github.com/coq/coq/pull/11606>`_, by Jason Gross).
+- **Fixed:**
+  Fields of a record tuple now link in coqdoc to their definition
+  (`#12027 <https://github.com/coq/coq/pull/12027>`_, fixes
+  `#3415 <https://github.com/coq/coq/issues/3415>`_,
+  by Hugo Herbelin).
+- **Fixed:**
+  ``coqdoc`` now reports the location of a mismatched opening ``[[``
+  instead of throwing an uninformative exception
+  (`#12037 <https://github.com/coq/coq/pull/12037>`_,
+  fixes `#9670 <https://github.com/coq/coq/issues/9670>`_,
+  by Xia Li-yao).
+- **Fixed:**
+  coqchk incorrectly reporting names from opaque modules as axioms
+  (`#12076 <https://github.com/coq/coq/pull/12076>`_,
+  by Pierre Roux; fixes `#5030 <https://github.com/coq/coq/issues/5030>`_).
+
+**CoqIDE**
+
+- **Removed:**
+  "Tactic" menu from CoqIDE which had been unmaintained for a number of years
+  (`#11414 <https://github.com/coq/coq/pull/11414>`_,
+  by Pierre-Marie Pédrot).
+- **Removed:**
+  "Revert all buffers" command from CoqIDE which had been broken for a long time
+  (`#11415 <https://github.com/coq/coq/pull/11415>`_,
+  by Pierre-Marie Pédrot).
+
+**Standard library**
+
+- **Changed:**
+  Notations :n:`[|@term|]` and :n:`[||@term||]` for morphisms from 63-bit
+  integers to :g:`Z` and :g:`zn2z int` have been removed in favor of
+  :n:`φ(@term)` and :n:`Φ(@term)` respectively. These notations were
+  breaking Ltac parsing (`#11686 <https://github.com/coq/coq/pull/11686>`_,
+  by Maxime Dénès).
+- **Changed:**
+  The names of ``Sorted_sort`` and ``LocallySorted_sort`` in ``Coq.Sorting.MergeSort``
+  have been swapped to appropriately reflect their meanings
+  (`#11885 <https://github.com/coq/coq/pull/11885>`_,
+  by Lysxia).
+- **Changed:**
+  Notations :g:`<=?` and :g:`<?` from ``Coq.Structures.Orders`` and
+  ``Coq.Sorting.Mergesort.NatOrder`` are now at level 70 rather than
+  35, so as to be compatible with the notations defined everywhere
+  else in the standard library.  This may require re-parenthesizing
+  some expressions.  These notations were breaking the ability to
+  import modules from the standard library that were otherwise
+  compatible (fixes `#11890
+  <https://github.com/coq/coq/issues/11890>`_, `#11891
+  <https://github.com/coq/coq/pull/11891>`_, by Jason Gross).
+- **Changed:**
+  The level of :g:`≡` in ``Coq.Numbers.Cyclic.Int63.Int63`` is now 70,
+  no associativity, in line with :g:`=`.  Note that this is a minor
+  incompatibility with developments that declare their own :g:`≡`
+  notation and import ``Int63`` (fixes `#11905
+  <https://github.com/coq/coq/issues/11905>`_, `#11909
+  <https://github.com/coq/coq/pull/11909>`_, by Jason Gross).
+- **Changed:**
+  No longer re-export ``ListNotations`` from ``Program`` (``Program.Syntax``)
+  (`#11992 <https://github.com/coq/coq/pull/11992>`_,
+  by Antonio Nikishaev).
+- **Changed:**
+  It is now possible to import the :g:`nsatz` machinery without
+  transitively depending on the axioms of the real numbers nor of
+  classical logic by loading ``Coq.nsatz.NsatzTactic`` rather than
+  ``Coq.nsatz.Nsatz``.  Note that some constants have changed kernel
+  names, living in ``Coq.nsatz.NsatzTactic`` rather than
+  ``Coq.nsatz.Nsatz``; this might cause minor incompatibilities that
+  can be fixed by actually running :g:`Import Nsatz` rather than
+  relying on absolute names (`#12073
+  <https://github.com/coq/coq/pull/12073>`_, by Jason Gross; fixes
+  `#5445 <https://github.com/coq/coq/issues/5445>`_).
+- **Changed:**
+  new lemma ``NoDup_incl_NoDup`` in ``List.v``
+  to remove useless hypothesis `NoDup l'` in ``Sorting.Permutation.NoDup_Permutation_bis``
+  (`#12120 <https://github.com/coq/coq/pull/12119>`_,
+  by Olivier Laurent).
+- **Changed:**
+  :cmd:`Fixpoints <Fixpoint>` of the standard library without a recursive call turned
+  into ordinary :cmd:`Definitions <Definition>`
+  (`#12121 <https://github.com/coq/coq/pull/12121>`_,
+  by Hugo Herbelin; fixes `#11903 <https://github.com/coq/coq/pull/11903>`_).
+- **Deprecated:**
+  ``Bool.leb`` in favor of ``Bool.le``. The definition of ``Bool.le``
+  is made local to avoid conflicts with ``Nat.le``. As a consequence,
+  previous calls to ``leb`` based on importing ``Bool`` should now be
+  qualified into ``Bool.le`` even if ``Bool`` is imported
+  (`#12162 <https://github.com/coq/coq/pull/12162>`_,
+  by Olivier Laurent).
+- **Added:** Theorem :g:`bezout_comm` for natural numbers
+  (`#11127 <https://github.com/coq/coq/pull/11127>`_, by Daniel de Rauglaudre).
+- **Added**
+  :g:`rew dependent` notations for the dependent version of
+  :g:`rew` in :g:`Coq.Init.Logic.EqNotations` to improve the display
+  and parsing of :g:`match` statements on :g:`Logic.eq` (`#11240
+  <https://github.com/coq/coq/pull/11240>`_, by Jason Gross).
+- **Added:**
+  Lemmas about lists:
+
+  - properties of ``In``: ``in_elt``, ``in_elt_inv``
+  - properties of ``nth``: ``app_nth2_plus``, ``nth_middle``, ``nth_ext``
+  - properties of ``last``: ``last_last``, ``removelast_last``
+  - properties of ``remove``: ``remove_cons``, ``remove_app``, ``notin_remove``, ``in_remove``, ``in_in_remove``, ``remove_remove_comm``, ``remove_remove_eq``, ``remove_length_le``, ``remove_length_lt``
+  - properties of ``concat``: ``in_concat``, ``remove_concat``
+  - properties of ``map`` and ``flat_map``: ``map_last``, ``map_eq_cons``, ``map_eq_app``, ``flat_map_app``, ``flat_map_ext``, ``nth_nth_nth_map``
+  - properties of ``incl``: ``incl_nil_l``, ``incl_l_nil``, ``incl_cons_inv``, ``incl_app_app``, ``incl_app_inv``, ``remove_incl``, ``incl_map``, ``incl_filter``, ``incl_Forall_in_iff``
+  - properties of ``NoDup`` and ``nodup``: ``NoDup_rev``, ``NoDup_filter``, ``nodup_incl``
+  - properties of ``Exists`` and ``Forall``: ``Exists_nth``, ``Exists_app``, ``Exists_rev``, ``Exists_fold_right``, ``incl_Exists``, ``Forall_nth``, ``Forall_app``, ``Forall_elt``, ``Forall_rev``, ``Forall_fold_right``, ``incl_Forall``, ``map_ext_Forall``, ``Exists_or``, ``Exists_or_inv``, ``Forall_and``, ``Forall_and_inv``, ``exists_Forall``, ``Forall_image``, ``concat_nil_Forall``, ``in_flat_map_Exists``, ``notin_flat_map_Forall``
+  - properties of ``repeat``: ``repeat_cons``, ``repeat_to_concat``
+  - definitions and properties of ``list_sum`` and ``list_max``: ``list_sum_app``, ``list_max_app``, ``list_max_le``, ``list_max_lt``
+  - misc: ``elt_eq_unit``, ``last_length``, ``rev_eq_app``, ``removelast_firstn_len``, ``cons_seq``, ``seq_S``
+
+  (`#11249 <https://github.com/coq/coq/pull/11249>`_, `#12237 <https://github.com/coq/coq/pull/12237>`_,
+  by Olivier Laurent).
+- **Added:**
+  Well-founded induction principles for `nat`: ``lt_wf_rect1``, ``lt_wf_rect``, ``gt_wf_rect``, ``lt_wf_double_rect``
+  (`#11335 <https://github.com/coq/coq/pull/11335>`_,
+  by Olivier Laurent).
+- **Added:**
+  ``remove'`` and ``count_occ'`` over lists,
+  alternatives to ``remove`` and ``count_occ`` based on ``filter``
+  (`#11350 <https://github.com/coq/coq/pull/11350>`_,
+  by Yishuai Li).
+- **Added:**
+  Facts about ``N.iter`` and ``Pos.iter``:
+
+    - ``N.iter_swap_gen``, ``N.iter_swap``, ``N.iter_succ``, ``N.iter_succ_r``, ``N.iter_add``, ``N.iter_ind``, ``N.iter_invariant``;
+    - ``Pos.iter_succ_r``, ``Pos.iter_ind``.
+
+  (`#11880 <https://github.com/coq/coq/pull/11880>`_,
+  by Lysxia).
+- **Added:**
+  Facts about ``Permutation``:
+
+  - structure: ``Permutation_refl'``, ``Permutation_morph_transp``
+  - compatibilities: ``Permutation_app_rot``, ``Permutation_app_swap_app``, ``Permutation_app_middle``, ``Permutation_middle2``, ``Permutation_elt``, ``Permutation_Forall``, ``Permutation_Exists``, ``Permutation_Forall2``, ``Permutation_flat_map``, ``Permutation_list_sum``, ``Permutation_list_max``
+  - inversions: ``Permutation_app_inv_m``, ``Permutation_vs_elt_inv``, ``Permutation_vs_cons_inv``, ``Permutation_vs_cons_cons_inv``, ``Permutation_map_inv``, ``Permutation_image``, ``Permutation_elt_map_inv``
+  - length-preserving definition by means of transpositions ``Permutation_transp`` with associated properties: ``Permutation_transp_sym``, ``Permutation_transp_equiv``, ``Permutation_transp_cons``, ``Permutation_Permutation_transp``, ``Permutation_ind_transp``
+
+  (`#11946 <https://github.com/coq/coq/pull/11946>`_,
+  by Olivier Laurent).
+- **Added:**
+  Notations for sigma types: ``{ x & P & Q }``, ``{ ' pat & P }``, ``{ ' pat & P & Q }``
+  (`#11957 <https://github.com/coq/coq/pull/11957>`_,
+  by Olivier Laurent).
+- **Added:**
+  Order relations ``lt`` and ``compare`` added in ``Bool.Bool``.
+  Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx``
+  (`#12008 <https://github.com/coq/coq/pull/12008>`_,
+  by Olivier Laurent).
+- **Added:**
+  Properties of some operations on vectors:
+
+  - ``nth_order``: ``nth_order_hd``, ``nth_order_tl``, ``nth_order_ext``
+  - ``replace``: ``nth_order_replace_eq``, ``nth_order_replace_neq``, ``replace_id``, ``replace_replace_eq``, ``replace_replace_neq``
+  - ``map``: ``map_id``, ``map_map``, ``map_ext_in``, ``map_ext``
+  - ``Forall`` and ``Forall2``: ``Forall_impl``, ``Forall_forall``, ``Forall_nth_order``, ``Forall2_nth_order``
+
+  (`#12014 <https://github.com/coq/coq/pull/12014>`_,
+  by Olivier Laurent).
+- **Added:**
+  Lemmas
+  :g:`orb_negb_l`,
+  :g:`andb_negb_l`,
+  :g:`implb_true_iff`,
+  :g:`implb_false_iff`,
+  :g:`implb_true_r`,
+  :g:`implb_false_r`,
+  :g:`implb_true_l`,
+  :g:`implb_false_l`,
+  :g:`implb_same`,
+  :g:`implb_contrapositive`,
+  :g:`implb_negb`,
+  :g:`implb_curry`,
+  :g:`implb_andb_distrib_r`,
+  :g:`implb_orb_distrib_r`,
+  :g:`implb_orb_distrib_l` in library :g:`Bool`
+  (`#12018 <https://github.com/coq/coq/pull/12018>`_,
+  by Hugo Herbelin).
+- **Added:**
+  Definition and properties of cyclic permutations / circular shifts: ``CPermutation``
+  (`#12031 <https://github.com/coq/coq/pull/12031>`_,
+  by Olivier Laurent).
+- **Added:**
+  ``Structures.OrderedTypeEx.Ascii_as_OT``
+  (`#12044 <https://github.com/coq/coq/pull/12044>`_,
+  by formalize.eth (formalize@protonmail.com)).
+- **Fixed:**
+  Rewrote ``Structures.OrderedTypeEx.String_as_OT.compare``
+  to avoid huge proof terms
+  (`#12044 <https://github.com/coq/coq/pull/12044>`_,
+  by formalize.eth (formalize@protonmail.com);
+  fixes `#12015 <https://github.com/coq/coq/issues/12015>`_).
+
+**Reals library**
+
+- **Changed:**
+  Cleanup of names in the Reals theory: replaced `tan_is_inj` with
+  `tan_inj` and replaced `atan_right_inv` with `tan_atan` -
+  compatibility notations are provided. Moved various auxiliary lemmas
+  from `Ratan.v` to more appropriate places
+  (`#9803 <https://github.com/coq/coq/pull/9803>`_,
+  by Laurent Théry and Michael Soegtrop).
+- **Changed:**
+  Replace `CRzero` and `CRone` by `CR_of_Q 0` and `CR_of_Q 1` in
+  `ConstructiveReals`.  Use implicit arguments for
+  `ConstructiveReals`. Move `ConstructiveReals` into new directory
+  `Abstract`. Remove imports of implementations inside those
+  `Abstract` files. Move implementation by means of Cauchy sequences
+  in new directory `Cauchy`.  Split files `ConstructiveMinMax` and
+  `ConstructivePower`.
+
+  .. warning:: The constructive reals modules are marked as experimental.
+
+  (`#11725 <https://github.com/coq/coq/pull/11725>`_,
+  `#12287 <https://github.com/coq/coq/pull/12287>`_
+  and `#12288 <https://github.com/coq/coq/pull/12288>`_,
+  by Vincent Semeria).
+- **Removed:**
+  Type `RList` has been removed.  All uses have been replaced by `list R`.
+  Functions from `RList` named `In`, `Rlength`, `cons_Rlist`, `app_Rlist`
+  have also been removed as they are essentially the same as `In`, `length`,
+  `app`, and `map` from `List`, modulo the following changes:
+
+    - `RList.In x (RList.cons a l)` used to be convertible to
+      `(x = a) \\/ RList.In x l`,
+      but `List.In x (a :: l)` is convertible to
+      `(a = x) \\/ List.In l`.
+      The equality is reversed.
+    - `app_Rlist` and `List.map` take arguments in different order.
+
+  (`#11404 <https://github.com/coq/coq/pull/11404>`_,
+  by Yves Bertot).
+- **Added:**
+  inverse trigonometric functions `asin` and `acos` with lemmas for
+  the derivatives, bounds and special values of these functions; an
+  extensive set of identities between trigonometric functions and
+  their inverse functions; lemmas for the injectivity of sine and
+  cosine; lemmas on the derivative of the inverse of decreasing
+  functions and on the derivative of horizontally mirrored functions;
+  various generic auxiliary lemmas and definitions for `Rsqr`, `sqrt`,
+  `posreal` and others
+  (`#9803 <https://github.com/coq/coq/pull/9803>`_,
+  by Laurent Théry and Michael Soegtrop).
+
+**Infrastructure and dependencies**
+
+- **Changed:**
+  Minimal versions of dependencies for building the reference manual:
+  now requires Sphinx 2.3.1+, sphinx_rtd_theme 0.4.3+ and
+  sphinxcontrib-bibtex 0.4.2+
+  (`#12224 <https://github.com/coq/coq/pull/12224>`_,
+  by Jim Fehrle and Théo Zimmermann).
+- **Removed:**
+  Python 2 is not longer required in any part of the codebase
+  (`#11245 <https://github.com/coq/coq/pull/11245>`_,
+  by Emilio Jesus Gallego Arias).
+
+**Miscellaneous**
+
+- **Added:**
+  Support for better extraction of strings in OCaml and Haskell:
+  `ExtOcamlNativeString` provides bindings from the Coq `String` type to
+  the OCaml `string` type, and string literals can be extracted to literals,
+  both in OCaml and Haskell (`#10486
+  <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from
+  Maxime Dénès, review by Hugo Herbelin).
+- **Added:**
+  Backtrace information for tactics has been improved
+  (`#11755 <https://github.com/coq/coq/pull/11755>`_,
+  by Emilio Jesus Gallego Arias).
+- **Fixed:**
+  In Haskell extraction with ``ExtrHaskellString``, equality comparisons on
+  strings and characters are now guaranteed to be uniquely well-typed, even in
+  very polymorphic contexts under ``unsafeCoerce``; this is achieved by adding
+  type annotations to the extracted code, and by making ``ExtrHaskellString``
+  export ``ExtrHaskellBasic`` (`#12263
+  <https://github.com/coq/coq/pull/12263>`_, by Jason Gross, fixes `#12257
+  <https://github.com/coq/coq/issues/12257>`_ and `#12258
+  <https://github.com/coq/coq/issues/12258>`_).
+
 Version 8.11
 ------------
 
diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst
index b4b14fb392..f872c1b2e3 100644
--- a/doc/sphinx/using/tools/coqdoc.rst
+++ b/doc/sphinx/using/tools/coqdoc.rst
@@ -220,8 +220,10 @@ Identifiers from the |Coq| standard library are linked to the Coq website
 using command line options ``--no-externals`` and ``--coqlib``; see below.
 
 
-Hiding / Showing parts of the source.
-+++++++++++++++++++++++++++++++++++++
+.. _coqdoc-hide-show:
+
+Hiding / Showing parts of the source
+++++++++++++++++++++++++++++++++++++
 
 Some parts of the source can be hidden using command line options ``-g``
 and ``-l`` (see below), or using such comments: