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

7 files changed, 71 insertions, 76 deletions

diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index cb267576b2..7b8a86d1ab 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -31,9 +31,9 @@ A variable pattern matches any value, and the identifier is bound to
 that value. The pattern “``_``” (called “don't care” or “wildcard” symbol)
 also matches any value, but does not bind anything. It may occur an
 arbitrary number of times in a pattern. Alias patterns written
-:n:`(@pattern as @identifier)` are also accepted. This pattern matches the
-same values as ``pattern`` does and ``identifier`` is bound to the matched
-value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A
+:n:`(@pattern as @ident)` are also accepted. This pattern matches the
+same values as :token:`pattern` does and :token:`ident` is bound to the matched
+value. A pattern of the form :n:`@pattern | @pattern` is called disjunctive. A
 list of patterns separated with commas is also considered as a pattern
 and is called *multiple pattern*. However multiple patterns can only
 occur at the root of pattern matching equations. Disjunctions of
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index f523a39477..b7d05fd6ef 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.
 
@@ -47,30 +47,30 @@ extraction. They both display extracted term(s) inside |Coq|.
 All the following commands produce real ML files. User can choose to
 produce one monolithic file or one file per |Coq| library.
 
-.. cmd:: Extraction "@file" {+ @qualid }
+.. cmd:: Extraction @string {+ @qualid }
 
    Recursive extraction of all the mentioned objects and all
-   their dependencies in one monolithic `file`.
+   their dependencies in one monolithic file :token:`string`.
    Global and local identifiers are renamed according to the chosen ML
    language to fulfill its syntactic conventions, keeping original
    names as much as possible.
   
 .. cmd:: Extraction Library @ident
 
-   Extraction of the whole |Coq| library ``ident.v`` to an ML module
-   ``ident.ml``. In case of name clash, identifiers are here renamed
+   Extraction of the whole |Coq| library :n:`@ident.v` to an ML module
+   :n:`@ident.ml`. In case of name clash, identifiers are here renamed
    using prefixes ``coq_``  or ``Coq_`` to ensure a session-independent
    renaming.
 
 .. cmd:: Recursive Extraction Library @ident
 
-   Extraction of the |Coq| library ``ident.v`` and all other modules 
-   ``ident.v`` depends on.
+   Extraction of the |Coq| library :n:`@ident.v` and all other modules
+   :n:`@ident.v` depends on.
 
 .. cmd:: Separate Extraction {+ @qualid }
 
    Recursive extraction of all the mentioned objects and all
-   their dependencies, just as ``Extraction "file"``,
+   their dependencies, just as :n:`Extraction @string {+ @qualid }`,
    but instead of producing one monolithic file, this command splits
    the produced code in separate ML files, one per corresponding Coq
    ``.v`` file. This command is hence quite similar to
@@ -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..64e2d7c4ab 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:
 
 
@@ -40,20 +40,20 @@ In addition to these user-defined classes, we have two built-in classes:
 Formally, the syntax of a classes is defined as:
 
 .. productionlist::
-   class: qualid
-        : | `Sortclass`
-        : | `Funclass`
+   class: `qualid`
+        : | Sortclass
+        : | Funclass
 
 
 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
@@ -207,10 +202,10 @@ grammar of inductive types from Figure :ref:`vernacular` as follows:
    \comindex{CoInductive \mbox{\rm (and coercions)}}
 
 .. productionlist::
-   inductive : `Inductive` ind_body `with` ... `with` ind_body
-             : | `CoInductive` ind_body `with` ... `with` ind_body
-   ind_body : ident [binders] : term := [[|] constructor | ... | constructor]
-   constructor : ident [binders] [:[>] term]
+   inductive : Inductive `ind_body` with ... with `ind_body`
+             : | CoInductive `ind_body` with ... with `ind_body`
+   ind_body : `ident` [ `binders` ] : `term` := [[|] `constructor` | ... | `constructor` ]
+   constructor : `ident` [ `binders` ] [:[>] `term` ]
 
 Especially, if the extra ``>`` is present in a constructor
 declaration, this constructor is declared as a coercion.
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/program.rst b/doc/sphinx/addendum/program.rst
index e153c7cbe2..429dcbee69 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -181,7 +181,7 @@ Program Definition
 Program Fixpoint
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term
+.. cmd:: Program Fixpoint @ident @binders {? {@order}} : @type := @term
 
    The optional order annotation follows the grammar:
 
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