10 files changed, 49 insertions, 109 deletions
diff --git a/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst b/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst
new file mode 100644
index 0000000000..1aa57ff8b1
--- /dev/null
+++ b/doc/changelog/04-tactics/13761-remove_convert_concl_nc.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+  convert_concl_no_check.  Use :tacn:`change_no_check` instead
+  (`#13761 <https://github.com/coq/coq/pull/13761>`_,
+  by Jim Fehrle).
diff --git a/doc/changelog/04-tactics/13762-remove_double_induction.rst b/doc/changelog/04-tactics/13762-remove_double_induction.rst
new file mode 100644
index 0000000000..4ea54a1ab6
--- /dev/null
+++ b/doc/changelog/04-tactics/13762-remove_double_induction.rst
@@ -0,0 +1,9 @@
+- **Removed:**
+  double induction tactic.  Replace :n:`double induction @ident @ident`
+  with :n:`induction @ident; induction @ident` (or
+  :n:`induction @ident ; destruct @ident` depending on the exact needs).
+  Replace :n:`double induction @natural__1 @natural__2` with
+  :n:`induction @natural__1; induction natural__3` where :n:`natural__3` is the result
+  of :n:`natural__2 - natural__1`
+  (`#13762 <https://github.com/coq/coq/pull/13762>`_,
+  by Jim Fehrle).
diff --git a/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst b/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst
new file mode 100644
index 0000000000..84d6bdea89
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13758-remove_hide_obligations.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+  The Hide Obligations flag, deprecated in 8.12
+  (`#13758 <https://github.com/coq/coq/pull/13758>`_,
+  by Jim Fehrle).
diff --git a/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst b/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst
new file mode 100644
index 0000000000..fc6c88eab6
--- /dev/null
+++ b/doc/changelog/07-vernac-commands-and-options/13764-remove_add_injtyp.rst
@@ -0,0 +1,6 @@
+- **Removed:**
+  `Show Zify Spec`, `Add InjTyp` and 11 similar `Add *` commands.
+  For `Show Zify Spec`, use `Show Zify UnOpSpec` or `Show Zify BinOpSpec` instead.
+  For `Add *`, `Use Add Zify *` intead of `Add *`
+  (`#13764 <https://github.com/coq/coq/pull/13764>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 38c4886e0f..3bd85d29c8 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -315,68 +315,6 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    prints the list of types that supported by :tacn:`zify` i.e.,
    :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
 
-.. cmd:: Show Zify Spec
-
-   .. deprecated:: 8.13
-       Use :cmd:`Show Zify` ``UnOpSpec`` or :cmd:`Show Zify` ``BinOpSpec`` instead.
-
-.. cmd:: Add InjTyp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``InjTyp`` instead.
-
-.. cmd:: Add BinOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``BinOp`` instead.
-
-.. cmd:: Add BinOpSpec @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``BinOpSpec`` instead.
-
-.. cmd:: Add UnOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``UnOp`` instead.
-
-.. cmd:: Add UnOpSpec @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``UnOpSpec`` instead.
-
-.. cmd:: Add CstOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``CstOp`` instead.
-
-.. cmd:: Add BinRel @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``BinRel`` instead.
-
-.. cmd:: Add PropOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``PropOp`` instead.
-
-.. cmd:: Add PropBinOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``PropBinOp`` instead.
-
-.. cmd:: Add PropUOp @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``PropUOp`` instead.
-
-.. cmd:: Add Saturate @one_term
-
-   .. deprecated:: 8.13
-       Use :cmd:`Add Zify` ``Saturate`` instead.
-
-
-
 
 .. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#fnpsatz] Variants deal with equalities and strict inequalities.
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 2b24ced8a1..8f2b51ccce 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -320,14 +320,6 @@ optional tactic is replaced by the default one if not specified.
    (the default), or if the system should infer which obligations can be
    declared opaque.
 
-.. flag:: Hide Obligations
-
-   .. deprecated:: 8.12
-
-   Controls whether obligations appearing in the
-   term should be hidden as implicit arguments of the special
-   constant ``Program.Tactics.obligation``.
-
 The module :g:`Coq.Program.Tactics` defines the default tactic for solving
 obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also
 adds some useful notations, as documented in the file itself.
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index d9e4e4f2b3..58444e8e82 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -531,11 +531,11 @@ Commands and options
   .. _813HintWarning:
 
 - **Deprecated:**
-  The default value for hint locality is currently :attr:`local` in a section and
-  :attr:`global` otherwise, but is scheduled to change in a future release. For the
-  time being, adding hints outside of sections without specifying an explicit
-  locality is therefore triggering a deprecation warning. It is recommended to
-  use :attr:`export` whenever possible
+  Hint locality currently defaults to :attr:`local` in a section and
+  :attr:`global` otherwise, but this will change in a future release.
+  Hints added outside of sections without an explicit
+  locality now generate a deprecation warning. We recommend
+  using :attr:`export` where possible
   (`#13384 <https://github.com/coq/coq/pull/13384>`_,
   by Pierre-Marie Pédrot).
 - **Deprecated:**
@@ -1230,7 +1230,7 @@ Flags, options and attributes
   :attr:`universes(template)` and ``universes(notemplate)`` instead
   (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann).
 - **Deprecated:**
-  :flag:`Hide Obligations` 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
@@ -3191,7 +3191,7 @@ Other changes in 8.10+beta1
     by Maxime Dénès, review by Pierre-Marie Pédrot).
 
   - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a
-    documented replacement of :tacn:`convert_concl_no_check`
+    documented replacement of `convert_concl_no_check`
     (`#10012 <https://github.com/coq/coq/pull/10012>`_,
     `#10017 <https://github.com/coq/coq/pull/10017>`_,
     `#10053 <https://github.com/coq/coq/pull/10053>`_, and
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 766f7ab44e..72970f46b0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -498,10 +498,16 @@ one or more of its hypotheses.
 
    :n:`{? - } {+ @nat_or_var }`
      Selects the specified occurrences within a single goal or hypothesis.
-     Occurrences are numbered from left to right starting with 1 when the
-     goal is printed with the :flag:`Printing All` flag.  (In particular, occurrences
-     in :ref:`implicit arguments <ImplicitArguments>` and
-     :ref:`coercions <Coercions>` are counted but not shown by default.)
+     Occurrences are numbered starting with 1 following a depth-first traversal
+     of the term's expression, including occurrences in
+     :ref:`implicit arguments <ImplicitArguments>`
+     and :ref:`coercions <Coercions>` that are not displayed by default.
+     (Set the :flag:`Printing All` flag to show those in the printed term.)
+
+     For example, when matching the pattern `_ + _` in the term `(a + b) + c`,
+     occurrence 1 is `(...) + c` and
+     occurrence 2 is `(a + b)`.  When matching that pattern with term `a + (b + c)`,
+     occurrence 1 is `a + (...)` and occurrence 2 is `b + c`.
 
      Specifying `-` includes all occurrences *except* the ones listed.
 
@@ -2067,19 +2073,6 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    is the name given by :n:`intros until @natural` to the :n:`@natural`-th non-dependent
    premise of the goal.
 
-.. tacn:: double induction @ident @ident
-   :name: double induction
-
-   This tactic is deprecated and should be replaced by
-   :n:`induction @ident; induction @ident` (or
-   :n:`induction @ident ; destruct @ident` depending on the exact needs).
-
-.. tacv:: double induction @natural__1 @natural__2
-
-   This tactic is deprecated and should be replaced by
-   :n:`induction num1; induction num3` where :n:`num3` is the result
-   of :n:`num2 - num1`
-
 .. tacn:: dependent induction @ident
    :name: dependent induction
 
diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst
index d2e88261ae..30f7be5f13 100644
--- a/doc/sphinx/proofs/automatic-tactics/auto.rst
+++ b/doc/sphinx/proofs/automatic-tactics/auto.rst
@@ -285,9 +285,9 @@ Creating Hints
    .. deprecated:: 8.13
 
      The default value for hint locality will change in a future
-     release. For the time being, adding hints outside of sections without
-     specifying an explicit locality will trigger a deprecation
-     warning. We recommend you use :attr:`export` whenever possible.
+     release. Hints added outside of sections without an explicit
+     locality are now deprecated. We recommend using :attr:`export`
+     where possible.
 
    The `Hint` commands are:
 
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 8873d02888..663337bc64 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -91,7 +91,10 @@ Rewriting with Leibniz and setoid equality
      in the conclusion is replaced.
 
      If :n:`at @occs_nums` is specified, rewriting is always done with
-     :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality.
+     :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality,
+     which means that you must `Require Setoid` to use that form.
+     However, note that :tacn:`rewrite` (even when using setoid rewriting) and
+     :tacn:`setoid_rewrite` don't behave identically (as already mentioned above).
 
    :n:`by @ltac_expr3`
      If specified, is used to resolve all side conditions generated by the tactic.
@@ -338,13 +341,6 @@ Rewriting with definitional equality
            exact H.
          Qed.
 
-   .. tacn:: convert_concl_no_check @one_term
-
-      .. deprecated:: 8.11
-
-      Deprecated old name for :tacn:`change_no_check`. Does not support any of its
-      variants.
-
 .. _performingcomputations:
 
 Performing computations
@@ -890,10 +886,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
 Conversion tactics applied to hypotheses
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. tacn:: @tactic in {+, @ident}
-
-   Applies :token:`tactic` (any of the conversion tactics listed in this
-   section) to the hypotheses :n:`{+ @ident}`.
+   The form :n:`@tactic in {+, @ident }` applies :token:`tactic` (any of the
+   conversion tactics listed in this section) to the hypotheses :n:`{+ @ident}`.
 
    If :token:`ident` is a local definition, then :token:`ident` can be replaced by
    :n:`type of @ident` to address not the body but the type of the local