Closes #9118: single backticks are made equivalent to double backticks; try to fix all misuses.

5 files changed, 53 insertions, 58 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index f523a39477..a1a27a1186 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -28,7 +28,7 @@ Generating ML Code
 
 .. note::
 
-  In the following, a qualified identifier `qualid`
+  In the following, a qualified identifier :token:`qualid`
   can be used to refer to any kind of |Coq| global "object" : constant,
   inductive type, inductive constructor or module name.
 
@@ -214,9 +214,9 @@ principles of extraction (logical parts and types).
 .. cmd:: Extraction Implicit @qualid [ {+ @ident } ]
 
    This experimental command allows declaring some arguments of
-   `qualid` as implicit, i.e. useless in extracted code and hence to
-   be removed by extraction. Here `qualid` can be any function or
-   inductive constructor, and the given `ident` are the names of
+   :token:`qualid` as implicit, i.e. useless in extracted code and hence to
+   be removed by extraction. Here :token:`qualid` can be any function or
+   inductive constructor, and the given :token:`ident` are the names of
    the concerned arguments. In fact, an argument can also be referred
    by a number indicating its position, starting from 1.
 
@@ -253,7 +253,7 @@ what ML term corresponds to a given axiom.
 .. cmd:: Extract Constant @qualid => @string
 
    Give an ML extraction for the given constant.
-   The `string` may be an identifier or a quoted string.
+   The :token:`string` may be an identifier or a quoted string.
 
 .. cmd:: Extract Inlined Constant @qualid => @string
 
@@ -315,24 +315,24 @@ native boolean type instead of the |Coq| one. The syntax is the following:
 .. cmd:: Extract Inductive @qualid => @string [ {+ @string } ]
 
    Give an ML extraction for the given inductive type. You must specify
-   extractions for the type itself (first `string`) and all its
-   constructors (all the `string` between square brackets). In this form,
+   extractions for the type itself (first :token:`string`) and all its
+   constructors (all the :token:`string` between square brackets). In this form,
    the ML extraction must be an ML inductive datatype, and the native
    pattern matching of the language will be used.
 
 .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string
 
-   Same as before, with a final extra `string` that indicates how to
+   Same as before, with a final extra :token:`string` that indicates how to
    perform pattern matching over this inductive type. In this form,
    the ML extraction could be an arbitrary type.
-   For an inductive type with `k` constructors, the function used to
-   emulate the pattern matching should expect `(k+1)` arguments, first the `k`
+   For an inductive type with :math:`k` constructors, the function used to
+   emulate the pattern matching should expect :math:`k+1` arguments, first the :math:`k`
    branches in functional form, and then the inductive element to
    destruct. For instance, the match branch ``| S n => foo`` gives the
    functional form ``(fun n -> foo)``. Note that a constructor with no
    arguments is considered to have one unit argument, in order to block
    early evaluation of the branch: ``| O => bar`` leads to the functional
-   form ``(fun () -> bar)``. For instance, when extracting ``nat``
+   form ``(fun () -> bar)``. For instance, when extracting :g:`nat`
    into |OCaml| ``int``, the code to be provided has type:
    ``(unit->'a)->(int->'a)->int->'a``.
 
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 789890eab5..93375c42f1 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -25,10 +25,10 @@ typed modulo insertion of appropriate coercions. We allow to write:
 Classes
 -------
 
-A class with `n` parameters is any defined name with a type
-:g:`forall (x₁:A₁)..(xₙ:Aₙ),s` where ``s`` is a sort.  Thus a class with
+A class with :math:`n` parameters is any defined name with a type
+:n:`forall (@ident__1 : @type__1)..(@ident__n:@type__n), @sort`.  Thus a class with
 parameters is considered as a single class and not as a family of
-classes.  An object of a class ``C`` is any term of type :g:`C t₁ .. tₙ`.
+classes.  An object of a class is any term of type :n:`@class @term__1 .. @term__n`.
 In addition to these user-defined classes, we have two built-in classes:
 
 
@@ -49,11 +49,11 @@ Coercions
 ---------
 
 A name ``f`` can be declared as a coercion between a source user-defined class
-``C`` with `n` parameters and a target class ``D`` if one of these
+``C`` with :math:`n` parameters and a target class ``D`` if one of these
 conditions holds:
 
  * ``D`` is a user-defined class, then the type of ``f`` must have the form
-   :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where `m`
+   :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ), D u₁..uₘ` where :math:`m`
    is the number of parameters of ``D``.
  * ``D`` is ``Funclass``, then the type of ``f`` must have the form
    :g:`forall (x₁:A₁)..(xₙ:Aₙ)(y:C x₁..xₙ)(x:A), B`.
@@ -124,7 +124,7 @@ Declaring Coercions
 
 .. cmd:: Coercion @qualid : @class >-> @class
 
-  Declares the construction denoted by `qualid` as a coercion between
+  Declares the construction denoted by :token:`qualid` as a coercion between
   the two given classes.
 
   .. exn:: @qualid not declared.
@@ -159,23 +159,18 @@ Declaring Coercions
 
   .. cmdv:: Local Coercion @qualid : @class >-> @class
 
-     Declares the construction denoted by `qualid` as a coercion local to
+     Declares the construction denoted by :token:`qualid` as a coercion local to
      the current section.
 
-  .. cmdv:: Coercion @ident := @term
+  .. cmdv:: Coercion @ident := @term {? @type }
 
-     This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
-     and then declares `ident` as a coercion between it source and its target.
+     This defines :token:`ident` just like :n:`Definition @ident := term {? @type }`,
+     and then declares :token:`ident` as a coercion between it source and its target.
 
-  .. cmdv:: Coercion @ident := @term : @type
+  .. cmdv:: Local Coercion @ident := @term {? @type }
 
-     This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
-     and then declares `ident` as a coercion between it source and its target.
-
-  .. cmdv:: Local Coercion @ident := @term
-
-     This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
-     and then declares `ident` as a coercion between it source and its target.
+     This defines :token:`ident` just like :n:`Let @ident := @term  {? @type }`,
+     and then declares :token:`ident` as a coercion between it source and its target.
 
 Assumptions can be declared as coercions at declaration time.
 This extends the grammar of assumptions from
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 5d219ebd0d..fd66de427c 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -248,7 +248,7 @@ cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) +
 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
+.. [#] Support for :g:`nat` and :g:`N` is obtained by pre-processing the goal with
   the ``zify`` tactic.
 .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#] Variants deal with equalities and strict inequalities.
diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst
index e7a8c238ac..ed2e1ea58c 100644
--- a/doc/sphinx/addendum/nsatz.rst
+++ b/doc/sphinx/addendum/nsatz.rst
@@ -81,7 +81,7 @@ performed using :ref:`typeclasses`.
      produces a goal which states that :math:`c` is not zero.
 
    * `variables` is the list of the variables in the decreasing order in
-     which they will be used in the Buchberger algorithm. If `variables` = `(@nil R)`,
+     which they will be used in the Buchberger algorithm. If `variables` = :g:`(@nil R)`,
      then `lvar` is replaced by all the variables which are not in
      `parameters`.
 
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 5bab63f6d0..99d689132d 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -376,8 +376,8 @@ The syntax for adding a new ring is
    sign :n:`@term`
       allows :tacn:`ring_simplify` to use a minus operation when
       outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The
-      term `:n:`@term` is a proof that a given sign function indicates expressions
-      that are signed (`term` has to be a proof of ``Ring_theory.get_sign``). See
+      term :token:`term` is a proof that a given sign function indicates expressions
+      that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See
       ``plugins/setoid_ring/InitialRing.v`` for examples of sign function.
 
    div :n:`@term`
@@ -476,8 +476,8 @@ So now, what is the scheme for a normalization proof? Let p be the
 polynomial expression that the user wants to normalize. First a little
 piece of |ML| code guesses the type of `p`, the ring theory `T` to use, an
 abstract polynomial `ap` and a variables map `v` such that `p` is |bdi|-
-equivalent to ``(PEeval`` `v` `ap`\ ``)``. Then we replace it by ``(Pphi_dev`` `v`
-``(norm`` `ap`\ ``))``, using the main correctness theorem and we reduce it to a
+equivalent to `(PEeval v ap)`. Then we replace it by `(Pphi_dev v (norm ap))`,
+using the main correctness theorem and we reduce it to a
 concrete expression `p’`, which is the concrete normal form of `p`. This is summarized in this diagram:
 
 ========= ======  ====
@@ -540,15 +540,15 @@ Dealing with fields
 
 .. tacv:: field [{* @term}] 
 
-  decides the equality of two terms modulo
-  field operations and the equalities defined  
-  by the :n:`@term`\ s. Each :n:`@term` has to be a proof of some equality 
-  `m` ``=`` `p`, where `m` is a monomial (after “abstraction”), `p` a polynomial 
-  and ``=`` the corresponding equality of the field structure.
+   This tactic decides the equality of two terms modulo
+   field operations and the equalities defined
+   by the :token:`term`\s. Each :token:`term` has to be a proof of some equality
+   :g:`m = p`, where :g:`m` is a monomial (after “abstraction”), :g:`p` a polynomial
+   and :g:`=` the corresponding equality of the field structure.
 
 .. note:: 
 
-   rewriting works with the equality  `m` ``=`` `p` only if `p` is a polynomial since
+   Rewriting works with the equality  :g:`m = p` only if :g:`p` is a polynomial since
    rewriting is handled by the underlying ring tactic.
 
 .. tacv:: field_simplify
@@ -562,27 +562,28 @@ Dealing with fields
 
 .. tacv:: field_simplify [{* @term }] 
 
-  performs the simplification in the conclusion of the goal using the equalities 
-  defined by the :n:`@term`\ s.
+   This variant performs the simplification in the conclusion of the goal using the equalities
+   defined by the :token:`term`\s.
 
 .. tacv:: field_simplify [{* @term }] {* @term }
 
-   performs the simplification in the terms :n:`@terms`  of the conclusion of the goal
-   using the equalities defined by :n:`@term`\ s inside the brackets.
+   This variant performs the simplification in the terms :token:`term`\s  of the conclusion of the goal
+   using the equalities defined by :token:`term`\s inside the brackets.
 
-.. tacv :: field_simplify in @ident
+.. tacv:: field_simplify in @ident
 
-   performs the simplification in the assumption :n:`@ident`.
+   This variant performs the simplification in the assumption :token:`ident`.
 
-.. tacv :: field_simplify [{* @term }] in @ident 
+.. tacv:: field_simplify [{* @term }] in @ident
  
-   performs the simplification
-   in the assumption :n:`@ident` using the equalities defined by the :n:`@term`\ s.
+   This variant performs the simplification
+   in the assumption :token:`ident` using the equalities defined by the :token:`term`\s.
 
 .. tacv:: field_simplify [{* @term }] {* @term } in @ident
 
-   performs the simplification in the :n:`@term`\ s of the assumption :n:`@ident` using the
-   equalities defined by  the :n:`@term`\ s inside the brackets.
+   This variant performs the simplification in the :token:`term`\s of the
+   assumption :token:`ident` using the
+   equalities defined by the :token:`term`\s inside the brackets.
 
 .. tacv:: field_simplify_eq
 
@@ -591,18 +592,17 @@ Dealing with fields
 
 .. tacv:: field_simplify_eq [ {* @term }]
 
-   performs the simplification in
-   the conclusion of the goal using the equalities defined by 
-   :n:`@term`\ s.
+   This variant performs the simplification in
+   the conclusion of the goal using the equalities defined by :token:`term`\s.
 
 .. tacv:: field_simplify_eq in @ident
 
-   performs the simplification in the assumption :n:`@ident`.
+   This variant performs the simplification in the assumption :token:`ident`.
 
 .. tacv:: field_simplify_eq [{* @term}] in @ident
 
-   performs the simplification in the assumption :n:`@ident` using the equalities defined by
-   :n:`@terms`\ s and removing the denominator.
+   This variant performs the simplification in the assumption :token:`ident`
+   using the equalities defined by :token:`term`\s and removing the denominator.
 
 
 Adding a new field structure