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

10 files changed, 226 insertions, 233 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 01240a062c..a20b74822c 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -32,7 +32,7 @@ Names (link targets) are auto-generated for most simple objects, though they can
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
 - Vernac variants, tactic notations, and tactic variants do not have a default name.
 
-Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes)::
+Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the ``:undocumented:`` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes)::
 
    .. cmdv:: Lemma @ident {? @binders} : @type
              Remark @ident {? @binders} : @type
@@ -382,7 +382,7 @@ DO
 DON'T
   .. code::
 
-     This is equivalent to ``Axiom`` :token`ident` : :token:`term`.
+     This is equivalent to ``Axiom`` :token:`ident` : :token:`term`.
 
 ..
 
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 86914a71df..11f0cdc008 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -32,7 +32,7 @@ Names (link targets) are auto-generated for most simple objects, though they can
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
 - Vernac variants, tactic notations, and tactic variants do not have a default name.
 
-Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes)::
+Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the ``:undocumented:`` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes)::
 
    .. cmdv:: Lemma @ident {? @binders} : @type
              Remark @ident {? @binders} : @type
@@ -138,7 +138,7 @@ DO
 DON'T
   .. code::
 
-     This is equivalent to ``Axiom`` :token`ident` : :token:`term`.
+     This is equivalent to ``Axiom`` :token:`ident` : :token:`term`.
 
 ..
 
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
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index d98b8641e9..e681d0f3ff 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -147,7 +147,7 @@ exclude_patterns = [
 
 # The reST default role (used for this markup: `text`) to use for all
 # documents.
-#default_role = None
+default_role = 'literal'
 
 # Use the Coq domain
 primary_domain = 'coq'
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 562ed48171..376a6b8eed 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -46,25 +46,26 @@ in which case the correctness of :n:`@type__3` may rely on the instance :n:`@ter
 
    The set of rational numbers may be defined as:
 
-  .. coqtop:: reset all
+   .. coqtop:: reset all
 
-     Record Rat : Set := mkRat
-     {sign : bool;
-     top : nat;
-     bottom : nat;
-     Rat_bottom_cond : 0 <> bottom;
-     Rat_irred_cond :
-     forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}.
+      Record Rat : Set := mkRat
+       { sign : bool
+       ; top : nat
+       ; bottom : nat
+       ; Rat_bottom_cond : 0 <> bottom
+       ; Rat_irred_cond :
+           forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1
+       }.
 
-Remark here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` and ``Rat_irred_cond``
-depends on both ``top`` and ``bottom``.
+   Note here that the fields ``Rat_bottom_cond`` depends on the field ``bottom``
+   and ``Rat_irred_cond`` depends on both ``top`` and ``bottom``.
 
 Let us now see the work done by the ``Record`` macro. First the macro
 generates a variant type definition with just one constructor:
-:n:`Variant @ident {? @binders } : @sort := @ident₀ {? @binders }`.
+:n:`Variant @ident {? @binders } : @sort := @ident__0 {? @binders }`.
 
-To build an object of type :n:`@ident`, one should provide the constructor
-:n:`@ident₀` with the appropriate number of terms filling the fields of the record.
+To build an object of type :token:`ident`, one should provide the constructor
+:n:`@ident__0` with the appropriate number of terms filling the fields of the record.
 
 .. example::
 
@@ -129,7 +130,7 @@ This syntax can also be used for pattern matching.
      end).
 
 The macro generates also, when it is possible, the projection
-functions for destructuring an object of type `\ident`.  These
+functions for destructuring an object of type :token:`ident`. These
 projection functions are given the names of the corresponding
 fields. If a field is named `_` then no projection is built
 for it. In our example:
@@ -163,17 +164,17 @@ available:
 .. _record_projections_grammar:
 
   .. productionlist:: terms
-     projection : projection `.` ( `qualid` )
-          : | projection `.` ( `qualid` `arg` … `arg` )
-          : | projection `.` ( @`qualid` `term` … `term` )
+     projection : `term` `.` ( `qualid` )
+          : | `term` `.` ( `qualid` `arg` … `arg` )
+          : | `term` `.` ( @`qualid` `term` … `term` )
 
   Syntax of Record projections
 
-The corresponding grammar rules are given in the preceding grammar. When `qualid`
-denotes a projection, the syntax `term.(qualid)` is equivalent to `qualid term`,
-the syntax `term.(qualid` |arg_1| |arg_n| `)` to `qualid` |arg_1| `…` |arg_n| `term`,
-and the syntax `term.(@qualid` |term_1| |term_n| `)` to `@qualid` |term_1| `…` |term_n| `term`.
-In each case, `term` is the object projected and the
+The corresponding grammar rules are given in the preceding grammar. When :token:`qualid`
+denotes a projection, the syntax :n:`@term.(@qualid)` is equivalent to :n:`@qualid @term`,
+the syntax :n:`@term.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term`.
+and the syntax :n:`@term.(@@qualid {+ @term })` to :n:`@@qualid {+ @term } @term`.
+In each case, :token:`term` is the object projected and the
 other arguments are the parameters of the inductive type.
 
 
@@ -197,22 +198,22 @@ other arguments are the parameters of the inductive type.
   This message is followed by an explanation of this impossibility.
   There may be three reasons:
 
-  #. The name `ident` already exists in the environment (see :cmd:`Axiom`).
-  #. The body of `ident` uses an incorrect elimination for
-     `ident` (see :cmd:`Fixpoint` and :ref:`Destructors`).
-  #. The type of the projections `ident` depends on previous
+  #. The name :token:`ident` already exists in the environment (see :cmd:`Axiom`).
+  #. The body of :token:`ident` uses an incorrect elimination for
+     :token:`ident` (see :cmd:`Fixpoint` and :ref:`Destructors`).
+  #. The type of the projections :token:`ident` depends on previous
      projections which themselves could not be defined.
 
 .. exn:: Records declared with the keyword Record or Structure cannot be recursive.
 
-    The record name `ident` appears in the type of its fields, but uses
-    the keyword ``Record``. Use  the keyword ``Inductive`` or ``CoInductive`` instead.
+   The record name :token:`ident` appears in the type of its fields, but uses
+   the keyword ``Record``. Use  the keyword ``Inductive`` or ``CoInductive`` instead.
 
 .. exn:: Cannot handle mutually (co)inductive records.
 
-    Records  cannot  be  defined  as  part  of  mutually  inductive  (or
-    co-inductive) definitions,  whether with records only  or mixed with
-    standard definitions.
+   Records cannot be defined as part of mutually inductive (or
+   co-inductive) definitions, whether with records only or mixed with
+   standard definitions.
 
 During the definition of the one-constructor inductive definition, all
 the errors of inductive definitions, as described in Section
@@ -308,7 +309,7 @@ an object of the record type as arguments, and whose body is an
 application of the unfolded primitive projection of the same name. These
 constants are used when elaborating partial applications of the
 projection. One can distinguish them from applications of the primitive
-projection if the :flag`Printing Primitive Projection Parameters` option
+projection if the :flag:`Printing Primitive Projection Parameters` option
 is off: For a primitive projection application, parameters are printed
 as underscores while for the compatibility projections they are printed
 as usual.
@@ -380,7 +381,7 @@ we have the following equivalence
      | right _ => false
      end).
 
-Notice that the printing uses the :g:`if` syntax because `sumbool` is
+Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is
 declared as such (see :ref:`controlling-match-pp`).
 
 .. _irrefutable-patterns:
@@ -653,8 +654,7 @@ with applications only *at the end* of each branch.
 
 Function does not support partial application of the function being
 defined. Thus, the following example cannot be accepted due to the
-presence of partial application of `wrong` in the body of
-`wrong` :
+presence of partial application of :g:`wrong` in the body of :g:`wrong`:
 
 .. coqtop:: all
 
@@ -699,21 +699,22 @@ used by ``Function``. A more precise description is given below.
 
 .. cmdv:: Function @ident {* @binder } : @type := @term
 
-   Defines the not recursive function `ident` as if declared with `Definition`. Moreover
-   the following are defined:
+   Defines the not recursive function :token:`ident` as if declared with
+   :cmd:`Definition`. Moreover the following are defined:
 
-    + `ident_rect`, `ident_rec` and `ident_ind`, which reflect the pattern
-      matching structure of `term` (see :cmd:`Inductive`);
-    + The inductive `R_ident` corresponding to the graph of `ident` (silently);
-    + `ident_complete` and `ident_correct` which are inversion information
-      linking the function and its graph.
+    + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``,
+      which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`);
+    + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently);
+    + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which
+      are inversion information linking the function and its graph.
 
 .. cmdv:: Function @ident {* @binder } { struct @ident } : @type := @term
 
-   Defines the structural recursive function `ident` as if declared with ``Fixpoint``. Moreover the following are defined:
+   Defines the structural recursive function :token:`ident` as if declared
+   with :cmd:`Fixpoint`. Moreover the following are defined:
 
     + The same objects as above;
-    + The fixpoint equation of `ident`: `ident_equation`.
+    + The fixpoint equation of :token:`ident`: :n:`@ident_equation`.
 
 .. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term
           Function @ident {* @binder } { wf @term @ident } : @type := @term
@@ -722,16 +723,16 @@ used by ``Function``. A more precise description is given below.
    of the standard library must be loaded for this feature. The ``{}``
    annotation is mandatory and must be one of the following:
 
-    + ``{measure`` `term` `ident` ``}`` with `ident` being the decreasing argument
-      and `term` being a function from type of `ident` to ``nat`` for which
-      value on the decreasing argument decreases (for the ``lt`` order on ``nat``)
-      at each recursive call of `term`. Parameters of the function are
-      bound in `term`\ ;
-    + ``{wf`` `term` `ident` ``}`` with `ident` being the decreasing argument and
-      `term` an ordering relation on the type of `ident` (i.e. of type
+    + :n:`{measure @term @ident }` with :token:`ident` being the decreasing argument
+      and :token:`term` being a function from type of :token:`ident` to :g:`nat` for which
+      value on the decreasing argument decreases (for the :g:`lt` order on :g:`nat`)
+      at each recursive call of :token:`term`. Parameters of the function are
+      bound in :token:`term`;
+    + :n:`{wf @term @ident }` with :token:`ident` being the decreasing argument and
+      :token:`term` an ordering relation on the type of :token:`ident` (i.e. of type
       `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument
-      decreases at each recursive call of `term`. The order must be well-founded.
-      Parameters of the function are bound in `term`.
+      decreases at each recursive call of :token:`term`. The order must be well-founded.
+      Parameters of the function are bound in :token:`term`.
 
    Depending on the annotation, the user is left with some proof
    obligations that will be used to define the function. These proofs
@@ -770,42 +771,42 @@ Section :ref:`gallina-definitions`).
 
 .. cmd:: End @ident
 
-    This command closes the section named `ident`. After closing of the
-    section, the local declarations (variables and local definitions) get
-    *discharged*, meaning that they stop being visible and that all global
-    objects defined in the section are generalized with respect to the
-    variables and local definitions they each depended on in the section.
+   This command closes the section named :token:`ident`. After closing of the
+   section, the local declarations (variables and local definitions) get
+   *discharged*, meaning that they stop being visible and that all global
+   objects defined in the section are generalized with respect to the
+   variables and local definitions they each depended on in the section.
 
-    .. example::
+   .. example::
 
-        .. coqtop:: all
+      .. coqtop:: all
 
-           Section s1.
+         Section s1.
 
-           Variables x y : nat.
+         Variables x y : nat.
 
-           Let y' := y.
+         Let y' := y.
 
-           Definition x' := S x.
+         Definition x' := S x.
 
-           Definition x'' := x' + y'.
+         Definition x'' := x' + y'.
 
-           Print x'.
+         Print x'.
 
-           End s1.
+         End s1.
 
-           Print x'.
+         Print x'.
 
-          Print x''.
+         Print x''.
 
-    Notice the difference between the value of `x’` and `x’’` inside section
-    `s1` and outside.
+      Notice the difference between the value of :g:`x'` and :g:`x''` inside section
+      :g:`s1` and outside.
 
-    .. exn:: This is not the last opened section.
-       :undocumented:
+   .. exn:: This is not the last opened section.
+      :undocumented:
 
 .. note::
-   Most commands, like ``Hint``, ``Notation``, option management, … which
+   Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which
    appear inside a section are canceled when the section is closed.
 
 
@@ -816,26 +817,26 @@ The module system provides a way of packaging related elements
 together, as well as a means of massive abstraction.
 
   .. productionlist:: modules
-    module_type       : qualid
-                      : | `module_type` with Definition qualid := term
-                      : | `module_type` with Module qualid := qualid
-                      : | qualid qualid … qualid
-                      : | !qualid qualid … qualid
-    module_binding    : ( [Import|Export] ident … ident : module_type )
+    module_type       : `qualid`
+                      : | `module_type` with Definition `qualid` := `term`
+                      : | `module_type` with Module `qualid` := `qualid`
+                      : | `qualid` `qualid` … `qualid`
+                      : | !`qualid` `qualid` … `qualid`
+    module_binding    : ( [Import|Export] `ident` … `ident` : `module_type` )
     module_bindings   : `module_binding` … `module_binding`
-    module_expression : qualid … qualid
-                      : | !qualid … qualid
+    module_expression : `qualid` … `qualid`
+                      : | !`qualid` … `qualid`
 
   Syntax of modules
 
 In the syntax of module application, the ! prefix indicates that any
 `Inline` directive in the type of the functor arguments will be ignored
-(see the ``Module Type`` command below).
+(see the :cmd:`Module Type` command below).
 
 
 .. cmd:: Module @ident
 
-   This command is used to start an interactive module named `ident`.
+   This command is used to start an interactive module named :token:`ident`.
 
 .. cmdv:: Module @ident {* @module_binding}
 
@@ -848,21 +849,22 @@ In the syntax of module application, the ! prefix indicates that any
 
 .. cmdv:: Module @ident {* @module_binding} : @module_type
 
-   Starts an interactive functor with parameters given by the list of `module binding`, and output module
-   type `module_type`.
+   Starts an interactive functor with parameters given by the list of
+   :token:`module_bindings`, and output module type :token:`module_type`.
 
 .. cmdv:: Module @ident <: {+<: @module_type }
 
-   Starts an interactive module satisfying each `module_type`.
+   Starts an interactive module satisfying each :token:`module_type`.
 
  .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }.
 
-   Starts an interactive functor with parameters given by the list of `module_binding`. The output module type
-   is verified against each `module_type`.
+   Starts an interactive functor with parameters given by the list of
+   :token:`module_binding`. The output module type
+   is verified against each :token:`module_type`.
 
 .. cmdv:: Module [ Import | Export ]
 
-   Behaves like ``Module``, but automatically imports or exports the module.
+   Behaves like :cmd:`Module`, but automatically imports or exports the module.
 
 Reserved commands inside an interactive module
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -913,7 +915,7 @@ Reserved commands inside an interactive module
     .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression
 
        Defines a functor with parameters given by module_bindings (possibly none) with body :token:`module_expression`.
-       The body is checked against each |module_type_i|.
+       The body is checked against each :n:`@module_type__i`.
 
     .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression}
 
@@ -1052,8 +1054,8 @@ specification: the y component is dropped as well as the body of x.
 
    End SIG.
 
-The definition of ``N`` using the module type expression ``SIG`` with
-``Definition T := nat`` is equivalent to the following one:
+The definition of :g:`N` using the module type expression :g:`SIG` with
+:g:`Definition T := nat` is equivalent to the following one:
 
 .. coqtop:: all
 
@@ -1138,7 +1140,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified.
   #. Modules and module types can be nested components of each other.
   #. One can have sections inside a module or a module type, but not a
      module or a module type inside a section.
-  #. Commands like ``Hint`` or ``Notation`` can also appear inside modules and
+  #. Commands like :cmd:`Hint` or :cmd:`Notation` can also appear inside modules and
      module types. Note that in case of a module definition like:
 
   ::
@@ -1157,73 +1159,73 @@ component is equal ``nat`` and hence ``M1.T`` as specified.
 
 .. cmd:: Import @qualid
 
-    If `qualid` denotes a valid basic module (i.e. its module type is a
-    signature), makes its components available by their short names.
+   If :token:`qualid` denotes a valid basic module (i.e. its module type is a
+   signature), makes its components available by their short names.
 
-    .. example::
+   .. example::
 
-       .. coqtop:: reset all
+      .. coqtop:: reset all
 
-          Module Mod.
+         Module Mod.
 
-          Definition T:=nat.
+         Definition T:=nat.
 
-          Check T.
+         Check T.
 
-          End Mod.
+         End Mod.
 
-          Check Mod.T.
+         Check Mod.T.
 
-          Fail Check T.
+         Fail Check T.
 
-          Import Mod.
+         Import Mod.
 
-          Check T.
+         Check T.
 
-    Some features defined in modules are activated only when a module is
-    imported. This is for instance the case of notations (see :ref:`Notations`).
+   Some features defined in modules are activated only when a module is
+   imported. This is for instance the case of notations (see :ref:`Notations`).
 
-    Declarations made with the ``Local`` flag are never imported by the :cmd:`Import`
-    command. Such declarations are only accessible through their fully
-    qualified name.
+   Declarations made with the ``Local`` flag are never imported by the :cmd:`Import`
+   command. Such declarations are only accessible through their fully
+   qualified name.
 
-    .. example::
+   .. example::
 
-       .. coqtop:: all
+      .. coqtop:: all
 
-          Module A.
+         Module A.
 
-          Module B.
+         Module B.
 
-          Local Definition T := nat.
+         Local Definition T := nat.
 
-          End B.
+         End B.
 
-          End A.
+         End A.
 
-          Import A.
+         Import A.
 
-          Fail Check B.T.
+         Fail Check B.T.
 
-    .. cmdv:: Export @qualid
-       :name: Export
+   .. cmdv:: Export @qualid
+      :name: Export
 
-       When the module containing the command Export qualid
-       is imported, qualid is imported as well.
+      When the module containing the command ``Export`` qualid
+      is imported, qualid is imported as well.
 
-    .. exn:: @qualid is not a module.
-       :undocumented:
+      .. exn:: @qualid is not a module.
+         :undocumented:
 
-    .. warn:: Trying to mask the absolute name @qualid!
-       :undocumented:
+      .. warn:: Trying to mask the absolute name @qualid!
+         :undocumented:
 
 .. cmd:: Print Module @ident
 
-   Prints the module type and (optionally) the body of the module :n:`@ident`.
+   Prints the module type and (optionally) the body of the module :token:`ident`.
 
 .. cmd:: Print Module Type @ident
 
-   Prints the module type corresponding to :n:`@ident`.
+   Prints the module type corresponding to :token:`ident`.
 
 .. flag:: Short Module Printing
 
@@ -1374,7 +1376,7 @@ OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object
 files as described above. The OCaml loadpath is managed using
 the option ``-I`` `path` (in the OCaml world, there is neither a
 notion of logical name prefix nor a way to access files in
-subdirectories of path). See the command ``Declare`` ``ML`` ``Module`` in
+subdirectories of path). See the command :cmd:`Declare ML Module` in
 :ref:`compiled-files` to understand the need of the OCaml loadpath.
 
 See :ref:`command-line-options` for a more general view over the |Coq| command
@@ -1515,7 +1517,6 @@ possible, the correct argument will be automatically generated.
 
 .. exn:: Cannot infer a term for this placeholder.
    :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments)
-   :undocumented:
 
    |Coq| was not able to deduce an instantiation of a “_”.
 
@@ -1803,20 +1804,20 @@ Explicit applications
 In presence of non-strict or contextual argument, or in presence of
 partial applications, the synthesis of implicit arguments may fail, so
 one may have to give explicitly certain implicit arguments of an
-application. The syntax for this is ``(`` `ident` ``:=`` `term` ``)`` where `ident` is the
+application. The syntax for this is :n:`(@ident := @term)` where :token:`ident` is the
 name of the implicit argument and term is its corresponding explicit
 term. Alternatively, one can locally deactivate the hiding of implicit
-arguments of a function by using the notation `@qualid` |term_1| … |term_n|.
+arguments of a function by using the notation :n:`@qualid {+ @term }`.
 This syntax extension is given in the following grammar:
 
 .. _explicit_app_grammar:
 
   .. productionlist:: explicit_apps
-       term     : @ qualid term … `term`
-                : | @ qualid
-                : | qualid `argument` … `argument`
+       term     : @ `qualid` `term` … `term`
+                : | @ `qualid`
+                : | `qualid` `argument` … `argument`
        argument : `term`
-                : | (ident := `term`)
+                : | (`ident` := `term`)
 
   Syntax for explicitly giving implicit arguments
 
@@ -2208,13 +2209,10 @@ existential variable is represented by “?” followed by an identifier.
 
    Check identity _ (fun x => _).
 
-In the general case, when an existential variable ``?``\ `ident` appears
+In the general case, when an existential variable :n:`?@ident` appears
 outside of its context of definition, its instance, written under the
-form
-
-| ``{`` :n:`{*; @ident:=@term}` ``}``
-
-is appending to its name, indicating how the variables of its defining context are instantiated.
+form :n:`{ {*; @ident := @term} }` is appending to its name, indicating
+how the variables of its defining context are instantiated.
 The variables of the context of the existential variables which are
 instantiated by themselves are not written, unless the flag :flag:`Printing Existential Instances`
 is on (see Section :ref:`explicit-display-existentials`), and this is why an
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 4bc85f386d..a98a46ba21 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -274,8 +274,8 @@ Requests to the environment
 
       This searches for all statements or types of
       definition that contains a subterm that matches the pattern
-      `term_pattern` (holes of the pattern are either denoted by `_` or by
-      `?ident` when non linear patterns are expected).
+      :token:`term_pattern` (holes of the pattern are either denoted by `_` or by
+      :n:`?@ident` when non linear patterns are expected).
 
    .. cmdv:: Search { + [-]@term_pattern_string }
 
@@ -580,7 +580,7 @@ file is a particular case of module called *library file*.
    replayed nor rechecked.
 
    To locate the file in the file system, :n:`@qualid` is decomposed under the
-   form `dirpath.ident` and the file `ident.vo` is searched in the physical
+   form :n:`dirpath.@ident` and the file :n:`@ident.vo` is searched in the physical
    directory of the file system that is mapped in |Coq| loadpath to the
    logical path dirpath (see Section :ref:`libraries-and-filesystem`). The mapping between
    physical directories and logical names at the time of requiring the
@@ -611,7 +611,7 @@ file is a particular case of module called *library file*.
    .. cmdv:: Require [Import | Export] {+ @qualid }
 
       This loads the
-      modules named by the :n:`qualid` sequence and their recursive
+      modules named by the :token:`qualid` sequence and their recursive
       dependencies. If
       ``Import`` or ``Export`` is given, it also imports these modules and
       all the recursive dependencies that were marked or transitively marked
@@ -620,8 +620,8 @@ file is a particular case of module called *library file*.
    .. cmdv:: From @dirpath Require @qualid
 
       This command acts as :cmd:`Require`, but picks
-      any library whose absolute name is of the form dirpath.dirpath’.qualid
-      for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library
+      any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid`
+      for some :n:`@dirpath’`. This is useful to ensure that the :token:`qualid` library
       comes from a given package by making explicit its absolute root.
 
    .. exn:: Cannot load qualid: no physical path bound to dirpath.
@@ -637,21 +637,21 @@ file is a particular case of module called *library file*.
 
       The command tried to load library file :n:`@ident`.vo that
       depends on some specific version of library :n:`@qualid` which is not the
-      one already loaded in the current |Coq| session. Probably `ident.v` was
+      one already loaded in the current |Coq| session. Probably :n:`@ident.v` was
       not properly recompiled with the last version of the file containing
-      module :n:`@qualid`.
+      module :token:`qualid`.
 
    .. exn:: Bad magic number.
 
-      The file `ident.vo` was found but either it is not a
+      The file :n:`@ident.vo` was found but either it is not a
       |Coq| compiled module, or it was compiled with an incompatible
       version of |Coq|.
 
-   .. exn:: The file `ident.vo` contains library dirpath and not library dirpath’.
+   .. exn:: The file :n:`@ident.vo` contains library dirpath and not library dirpath’.
 
-      The library file `dirpath’` is indirectly required by the
+      The library file :n:`@dirpath’` is indirectly required by the
       ``Require`` command but it is bound in the current loadpath to the
-      file `ident.vo` which was bound to a different library name `dirpath` at
+      file :n:`@ident.vo` which was bound to a different library name :token:`dirpath` at
       the time it was compiled.
 
 
@@ -675,10 +675,10 @@ file is a particular case of module called *library file*.
 .. cmd:: Declare ML Module {+ @string }
 
    This commands loads the OCaml compiled files
-   with names given by the :n:`@string` sequence
+   with names given by the :token:`string` sequence
    (dynamic link). It is mainly used to load tactics dynamically. The
    files are searched into the current OCaml loadpath (see the
-   command ``Add ML Path`` in Section :ref:`libraries-and-filesystem`).
+   command :cmd:`Add ML Path`).
    Loading of OCaml files is only possible under the bytecode version of
    ``coqtop`` (i.e. ``coqtop`` called with option ``-byte``, see chapter
    :ref:`thecoqcommands`), or when |Coq| has been compiled with a
@@ -698,9 +698,9 @@ file is a particular case of module called *library file*.
 
 .. cmd:: Print ML Modules
 
-   This prints the name of all OCaml modules loaded with ``Declare
-   ML Module``. To know from where these module were loaded, the user
-   should use the command ``Locate File`` (see :ref:`here <locate-file>`)
+   This prints the name of all OCaml modules loaded with :cmd:`Declare ML Module`.
+   To know from where these module were loaded, the user
+   should use the command :cmd:`Locate File`.
 
 
 .. _loadpath:
@@ -721,7 +721,7 @@ the toplevel, and using them in source files is discouraged.
 
 .. cmd:: Cd @string
 
-   This command changes the current directory according to :n:`@string` which
+   This command changes the current directory according to :token:`string` which
    can be any valid path.
 
    .. cmdv:: Cd
@@ -732,24 +732,24 @@ the toplevel, and using them in source files is discouraged.
 .. cmd:: Add LoadPath @string as @dirpath
 
    This command is equivalent to the command line option
-   ``-Q`` :n:`@string` :n:`@dirpath`. It adds the physical directory string to the current
+   :n:`-Q @string @dirpath`. It adds the physical directory string to the current
    |Coq| loadpath and maps it to the logical directory dirpath.
 
    .. cmdv:: Add LoadPath @string
 
-      Performs as Add LoadPath :n:`@string` as :n:`@dirpath` but
+      Performs as :n:`Add LoadPath @string @dirpath` but
       for the empty directory path.
 
 
 .. cmd:: Add Rec LoadPath @string as @dirpath
 
    This command is equivalent to the command line option
-   ``-R`` :n:`@string` :n:`@dirpath`. It adds the physical directory string and all its
+   :n:`-R @string @dirpath`. It adds the physical directory string and all its
    subdirectories to the current |Coq| loadpath.
 
    .. cmdv:: Add Rec LoadPath @string
 
-      Works as :cmd:`Add Rec LoadPath` :n:`@string` as :n:`@dirpath` but for the empty
+      Works as :n:`Add Rec LoadPath @string as @dirpath` but for the empty
       logical directory path.
 
 
@@ -792,7 +792,7 @@ the toplevel, and using them in source files is discouraged.
 .. cmd:: Locate File @string
 
    This command displays the location of file string in the current
-   loadpath. Typically, string is a .cmo or .vo or .v file.
+   loadpath. Typically, string is a ``.cmo`` or ``.vo`` or ``.v`` file.
 
 
 .. cmd:: Locate Library @dirpath
@@ -858,7 +858,7 @@ interactively, they cannot be part of a vernacular file loaded via
    state label is an integer which grows after each successful command.
    It is displayed in the prompt when in -emacs mode. Just as :cmd:`Back` (see
    above), the :cmd:`BackTo` command now handles proof states. For that, it may
-   have to undo some extra commands and end on a state `num′ ≤ num` if
+   have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if
    necessary.
 
    .. cmdv:: Backtrack @num @num @num
@@ -1157,7 +1157,7 @@ described first.
 
    This command allows giving a short name to a reduction expression, for
    instance lazy beta delta [foo bar]. This short name can then be used
-   in ``Eval`` :n:`@ident` ``in`` ... or ``eval`` directives. This command
+   in :n:`Eval @ident in` or ``eval`` directives. This command
    accepts the
    Local modifier, for discarding this reduction name at the end of the
    file or module. For the moment the name cannot be qualified. In
@@ -1165,7 +1165,7 @@ described first.
    functor applications will be refused if these declarations are not
    local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but
    nothing prevents the user to also perform a
-   ``Ltac`` `ident` ``:=`` `convtactic`.
+   :n:`Ltac @ident := @convtactic`.
 
    .. seealso:: :ref:`performingcomputations`