6 files changed, 15 insertions, 50 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index c0a57763b9..5d219ebd0d 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -35,7 +35,7 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``.
 
 
 The tactics solve propositional formulas parameterized by atomic
-arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}.
+arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`.
 The syntax of the formulas is the following:
 
  .. productionlist:: `F`
@@ -46,8 +46,8 @@ The syntax of the formulas is the following:
 where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the
 operators :math:`−, +, ×` are respectively subtraction, addition, and product;
 :math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition.
-For :math:`\mathbb{Q}`, equality is not Leibniz equality = but the equality of
-rationals ==.
+For :math:`\mathbb{Q}`, equality is not Leibniz equality ``=`` but the equality of
+rationals ``==``.
 
 For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational
 constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the
@@ -58,7 +58,7 @@ following expressions:
    c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c
 
 where :math:`z` is a constant in :math:`\mathbb{Z}` and :math:`q` is a constant in :math:`\mathbb{Q}`.
-This includes integer constants written using the decimal notation, *i.e.*, c%R.
+This includes integer constants written using the decimal notation, *i.e.*, ``c%R``.
 
 
 *Positivstellensatz* refutations
@@ -94,7 +94,7 @@ general form :math:`(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False}` and
 
 For each conjunct :math:`C_i`, the tactic calls an oracle which searches for
 :math:`-1` within the cone. Upon success, the oracle returns a *cone
-expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`)
+expression* that is normalized by the :tacn:`ring` tactic (see :ref:`theringandfieldtacticfamilies`)
 and checked to be :math:`-1`.
 
 `lra`: a decision procedure for linear real and rational arithmetic
@@ -245,11 +245,11 @@ proof by abstracting monomials by variables.
 As shown, such a goal is solved by ``intro x. psatz Z 2.``. The oracle returns the
 cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + -x^2`
 (polynomial hypotheses are printed in bold). By construction, this expression
-belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running `ring` we
+belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we
 obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 
 .. [#] Support for `nat` and :math:`\mathbb{N}` is obtained by pre-processing the goal with
-  the `zify` tactic.
+  the ``zify`` tactic.
 .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#] Variants deal with equalities and strict inequalities.
 .. [#] In practice, the oracle might fail to produce such a refutation.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 9dae7fd102..391afcb1f7 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2155,6 +2155,12 @@ If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
 language, and can be processed by Graphviz tools. The format is
 unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
 
+.. cmdv:: Print Universes Subgraph(@names)
+
+Prints the graph restricted to the requested names (adjusting
+constraints to preserve the implied transitive constraints between
+kept universes).
+
 .. _existential-variables:
 
 Existential variables
@@ -2247,7 +2253,3 @@ expression as described in :ref:`ltac`.
 This construction is useful when one wants to define complicated terms
 using highly automated tactics without resorting to writing the proof-term
 by means of the interactive proof engine.
-
-This mechanism is comparable to the ``Declare Implicit Tactic`` command
-defined at :ref:`tactics-implicit-automation`, except that the used
-tactic is local to each hole instead of being declared globally.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 741f9fe5b0..0b059f92ee 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -758,18 +758,6 @@ Controlling the effect of proof editing commands
    available hypotheses.
 
 
-.. flag:: Automatic Introduction
-
-   This option controls the way binders are handled
-   in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the
-   option is on, which is the default, binders are automatically put in
-   the local context of the goal to prove.
-
-   When the option is off, binders are discharged on the statement to be
-   proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`)
-   has to be used to move the assumptions to the local context.
-
-
 .. flag:: Nested Proofs Allowed
 
    When turned on (it is off by default), this option enables support for nested
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 457f9b2efa..041f1bc966 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3745,32 +3745,6 @@ Setting implicit automation tactics
 
       Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode`
 
-   .. cmd:: Declare Implicit Tactic @tactic
-
-      This command declares a tactic to be used to solve implicit arguments
-      that Coq does not know how to solve by unification. It is used every
-      time the term argument of a tactic has one of its holes not fully
-      resolved.
-
-      .. deprecated:: 8.9
-
-         This command is deprecated. Use :ref:`typeclasses <typeclasses>` or
-         :ref:`tactics-in-terms <tactics-in-terms>` instead.
-
-      .. example::
-
-         .. coqtop:: all
-
-            Parameter quo : nat -> forall n:nat, n<>0 -> nat.
-            Notation "x // y" := (quo x y _) (at level 40).
-            Declare Implicit Tactic assumption.
-            Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }.
-            intros.
-            exists (n // m).
-
-         The tactic ``exists (n // m)`` did not fail. The hole was solved
-         by ``assumption`` so that it behaved as ``exists (quo n m H)``.
-
 .. _decisionprocedures:
 
 Decision procedures
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index eacd7b4676..8f76085d88 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -167,7 +167,7 @@ Combined Scheme
 
     Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind.
 
-  The type of tree_forest_mutrec will be:
+  The type of tree_forest_mutind will be:
 
   .. coqtop:: all
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 64164cc56f..4fc9bf9e19 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -571,6 +571,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/Sqrt_reg.v
     theories/Reals/Rlogic.v
     (theories/Reals/Reals.v)
+    theories/Reals/Runcountable.v
   </dd>
 
   <dt> <b>Program</b>: