Uniformized many spelling variants. Added .. warning:: and .. seealso:: directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.

3 files changed, 31 insertions, 19 deletions

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 4e42bddee2..9498f37c7e 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -104,8 +104,12 @@ The following command-line options are recognized by the commands ``coqc``
 and ``coqtop``, unless stated otherwise:
 
 :-I *directory*, -include *directory*: Add physical path *directory*
-  to the OCaml loadpath. See also: :ref:`names-of-libraries` and the
-  command Declare ML Module Section :ref:`compiled-files`.
+  to the OCaml loadpath.
+
+  .. seealso::
+
+     :ref:`names-of-libraries` and the
+     command Declare ML Module Section :ref:`compiled-files`.
 :-Q *directory* dirpath: Add physical path *directory* to the list of
   directories where |Coq| looks for a file and bind it to the logical
   directory *dirpath*. The subdirectory structure of *directory* is
@@ -115,14 +119,17 @@ and ``coqtop``, unless stated otherwise:
   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
+  layout (within the limit of 255 bytes per filename), the default on
   NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to
   disallow two files differing only in the case in the same directory.
-  See also: Section :ref:`names-of-libraries`.
+
+  .. seealso:: Section :ref:`names-of-libraries`.
 :-R *directory* dirpath: Do as -Q *directory* dirpath but make the
   subdirectory structure of *directory* recursively visible so that the
   recursive contents of physical *directory* is available from |Coq| using
-  short or partially qualified names. See also: Section :ref:`names-of-libraries`.
+  short or partially qualified names.
+
+  .. seealso:: Section :ref:`names-of-libraries`.
 :-top dirpath: Set the toplevel module name to dirpath instead of Top.
   Not valid for `coqc` as the toplevel module name is inferred from the
   name of the output file.
@@ -168,11 +175,16 @@ and ``coqtop``, unless stated otherwise:
 :-emacs, -ide-slave: Start a special toplevel to communicate with a
   specific IDE.
 :-impredicative-set: Change the logical theory of |Coq| by declaring the
-   sort Set impredicative. Warning: This is known to be inconsistent with some
-   standard axioms of classical mathematics such as the functional
-   axiom of choice or the principle of description.
-:-type-in-type: Collapse the universe hierarchy of |Coq|. Warning: This makes the logic
-   inconsistent.
+   sort Set impredicative.
+
+   .. warning::
+
+      This is known to be inconsistent with some
+      standard axioms of classical mathematics such as the functional
+      axiom of choice or the principle of description.
+:-type-in-type: Collapse the universe hierarchy of |Coq|.
+
+  .. warning:: This makes the logic inconsistent.
 :-mangle-names *ident*: Experimental: Do not depend on this option. Replace
   Coq's auto-generated name scheme with names of the form *ident0*, *ident1*,
   etc. The command ``Set Mangle Names`` turns the behavior on in a document,
@@ -208,7 +220,7 @@ The ``coqchk`` command takes a list of library paths as argument, described eith
 by their logical name or by their physical filename, hich must end in ``.vo``. The
 corresponding compiled libraries (``.vo`` files) are searched in the path,
 recursively processing the libraries they depend on. The content of all these
-libraries is then type-checked. The effect of ``coqchk`` is only to return with
+libraries is then type checked. The effect of ``coqchk`` is only to return with
 normal exit code in case of success, and with positive exit code if an error has
 been found. Error messages are not deemed to help the user understand what is
 wrong. In the current version, it does not modify the compiled libraries to mark
@@ -248,15 +260,15 @@ the following: assuming that ``coqchk`` is called with argument ``M``, option
 ``-norec N``, and ``-admit A``. Let us write :math:`\overline{S}` for the
 set of reflexive transitive dependencies of set :math:`S`. Then:
 
-+ Modules :math:`C = \overline{M} \backslash \overline{A} \cup M \cup N` are loaded and type-checked before being added
++ Modules :math:`C = \overline{M} \backslash \overline{A} \cup M \cup N` are loaded and type checked before being added
   to the context.
 + And :math:`M \cup N \backslash C` is the set of modules that are loaded and added to the
-  context without type-checking. Basic integrity checks (checksums) are
+  context without type checking. Basic integrity checks (checksums) are
   nonetheless performed.
 
 As a rule of thumb, -admit can be used to tell Coq that some libraries
 have already been checked. So ``coqchk A B`` can be split in ``coqchk A`` &&
-``coqchk B -admit A`` without type-checking any definition twice. Of
+``coqchk B -admit A`` without type checking any definition twice. Of
 course, the latter is slightly slower since it makes more disk access.
 It is also less secure since an attacker might have replaced the
 compiled library ``A`` after it has been read by the first command, but
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index f7f442092f..bc6a074a27 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -12,7 +12,7 @@ file, executing corresponding commands or undoing them respectively.
 
 |CoqIDE| is run by typing the command `coqide` on the command line.
 Without argument, the main screen is displayed with an “unnamed
-buffer”, and with a file name as argument, another buffer displaying
+buffer”, and with a filename as argument, another buffer displaying
 the contents of that file. Additionally, `coqide` accepts the same
 options as `coqtop`, given in :ref:`thecoqcommands`, the ones having obviously
 no meaning for |CoqIDE| being ignored.
@@ -92,7 +92,7 @@ buffers (left and right arrows); an "information" button; and a "gears" button.
 
 The "information" button is described in Section :ref:`try-tactics-automatically`.
 
-The "gears" button submits proof terms to the |Coq| kernel for type-checking.
+The "gears" button submits proof terms to the |Coq| kernel for type checking.
 When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`),
 proofs may have been completed without kernel-checking of generated proof terms.
 The presence of unchecked proof terms is indicated by ``Qed`` statements that
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index e779515a00..218a19c2e5 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -43,7 +43,7 @@ Building a |Coq| project with coq_makefile
 The majority of |Coq| projects are very similar: a collection of ``.v``
 files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of
 metadata needed in order to build the project are the command line
-options to ``coqc`` (e.g. ``-R``, ``-I``, see also: Section
+options to ``coqc`` (e.g. ``-R``, ``-I``, see also: section
 :ref:`command-line-options`). Collecting the list of files and options is the job
 of the ``_CoqProject`` file.
 
@@ -107,7 +107,7 @@ decide how to build them. In particular:
 
 The use of ``.mlpack`` files has to be preferred over ``.mllib`` files,
 since it results in a “packed” plugin: All auxiliary modules (as
-``Baz`` and ``Bazaux``) are hidden inside the plugin’s “name space”
+``Baz`` and ``Bazaux``) are hidden inside the plugin’s "namespace"
 (``Qux_plugin``). This reduces the chances of begin unable to load two
 distinct plugins because of a clash in their auxiliary module names.
 
@@ -773,7 +773,7 @@ Command line options
     preamble, right before ``\begin{document}`` (meaningless with ``-html``).
   :--vernac-file file,--tex-file file: Considers the file ‘file’
     respectively as a ``.v`` (or ``.g``) file or a ``.tex`` file.
-  :--files-from file: Read file names to be processed from the file ‘file’ as if
+  :--files-from file: Read filenames to be processed from the file ‘file’ as if
     they were given on the command line. Useful for program sources split
     up into several directories.
   :-q, --quiet: Be quiet. Do not print anything except errors.