[Sphinx] Fix all remaining warnings.

3 files changed, 24 insertions, 25 deletions

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 9f485f496..93dcfca4b 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -106,7 +106,7 @@ and ``coqtop``, unless stated otherwise:
   recursively available from |Coq| using absolute names (extending the
   dirpath prefix) (see Section :ref:`qualified-names`).Note that only those
   subdirectories and files which obey the lexical conventions of what is
-  an ident (see Section :ref:`TODO-1.1`) are taken into account. Conversely, the
+  an :n:`@ident` are taken into account. Conversely, the
   underlying file systems or operating systems may be more restrictive
   than |Coq|. While Linux’s ext4 file system supports any |Coq| recursive
   layout (within the limit of 255 bytes per file name), the default on
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index 3d144b1d6..f9903e610 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -150,8 +150,6 @@ arguments.
 Queries
 ------------
 
-.. _coqide_queryselected:
-
 .. image:: ../_static/coqide-queries.png
    :alt: |CoqIDE| queries
 
@@ -161,7 +159,7 @@ writing them in scripts, |CoqIDE| offers a *query pane*. The query pane can be
 displayed on demand by using the ``View`` menu, or using the shortcut ``F1``.
 Queries can also be performed by selecting a particular phrase, then choosing an
 item from the ``Queries`` menu. The response then appears in the message window.
-Figure :ref:`fig:queryselected` shows the result after selecting of the phrase
+The image above shows the result after selecting of the phrase
 ``Nat.mul`` in the script window, and choosing ``Print`` from the ``Queries``
 menu.
 
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 48d58c473..59867988a 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -114,9 +114,7 @@ distinct plugins because of a clash in their auxiliary module names.
 .. _coqmakefilelocal:
 
 CoqMakefile.local
-+++++++++++++++++
-
-
+~~~~~~~~~~~~~~~~~
 
 The optional file ``CoqMakefile.local`` is included by the generated
 file ``CoqMakefile``. It can contain two kinds of directives.
@@ -190,7 +188,7 @@ The following makefile rules can be extended.
   target.
 
 Timing targets and performance testing
-++++++++++++++++++++++++++++++++++++++
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The generated ``Makefile`` supports the generation of two kinds of timing
 data: per-file build-times, and per-line times for an individual file.
@@ -365,7 +363,7 @@ line timing data:
 
 
 Reusing/extending the generated Makefile
-++++++++++++++++++++++++++++++++++++++++
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Including the generated makefile with an include directive is
 discouraged. The contents of this file, including variable names and
@@ -408,8 +406,8 @@ have a generic target for invoking unknown targets.
 
 
 
-Building a subset of the targets with -j
-++++++++++++++++++++++++++++++++++++++++
+Building a subset of the targets with ``-j``
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 To build, say, two targets foo.vo and bar.vo in parallel one can use
 ``make only TGTS="foo.vo bar.vo" -j``.
@@ -540,27 +538,28 @@ Initially, the pretty-printing table contains the following mapping:
 `->`  →       `<-`   ←       `*`   ×
 `<=`  ≤       `>=`   ≥       `=>`  ⇒
 `<>`  ≠       `<->`  ↔       `|-`  ⊢
-`\/`  ∨       `/\`   ∧       `~`   ¬
+`\/`  ∨       `/\\`   ∧       `~`   ¬
 ==== === ==== ===== === ==== ==== ===
 
 Any of these can be overwritten or suppressed using the printing
 commands.
 
-.. note ::
-  The recognition of tokens is done by a (``ocaml``) lex
-  automaton and thus applies the longest-match rule. For instance, `->~`
-  is recognized as a single token, where |Coq| sees two tokens. It is the
-  responsibility of the user to insert space between tokens *or* to give
-  pretty-printing rules for the possible combinations, e.g.
+.. note::
 
-  ::
+   The recognition of tokens is done by a (``ocaml``) lex
+   automaton and thus applies the longest-match rule. For instance, `->~`
+   is recognized as a single token, where |Coq| sees two tokens. It is the
+   responsibility of the user to insert space between tokens *or* to give
+   pretty-printing rules for the possible combinations, e.g.
+
+   ::
 
       (** printing ->~ %\ensuremath{\rightarrow\lnot}% *)
 
 
 
-Sections.
-+++++++++
+Sections
+++++++++
 
 Sections are introduced by 1 to 4 leading stars (i.e. at the beginning
 of the line) followed by a space. One star is a section, two stars a
@@ -569,7 +568,7 @@ line.
 
 .. example::
 
-  ::
+   ::
 
           (** * Well-founded relations
 
@@ -805,9 +804,10 @@ Command line options
     directory  ``coqdir`` (similarly to |Coq| option ``-R``).
 
     .. note::
-      option ``-R`` only has
-      effect on the files *following* it on the command line, so you will
-      probably need to put this option first.
+
+       option ``-R`` only has
+       effect on the files *following* it on the command line, so you will
+       probably need to put this option first.
 
 
 **Title options**
@@ -821,6 +821,7 @@ Command line options
      beginning of each file is checked for a comment of the form:
 
      ::
+
         (** * ModuleName : text *)
 
      where ``ModuleName`` must be the name of the file. If it is present, the