Improved grammar and spelling for chapters 'Utilities' and 'CoqIDE' of the Reference Manual.

2 files changed, 43 insertions, 45 deletions

diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index f9903e6104..f7f442092f 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -27,7 +27,7 @@ is shown in the figure :ref:`CoqIDE main screen <coqide_mainscreen>`.
 At the top is a menu bar, and a tool bar
 below it. The large window on the left is displaying the various
 *script buffers*. The upper right window is the *goal window*, where
-goals to prove are displayed. The lower right window is the *message
+goals to be proven are displayed. The lower right window is the *message
 window*, where various messages resulting from commands are displayed.
 At the bottom is the status bar.
 
@@ -62,8 +62,8 @@ In the figure :ref:`CoqIDE main screen <coqide_mainscreen>`,
 the running buffer is `Fermat.v`, all commands until
 the ``Theorem`` have been already executed, and the user tried to go
 forward executing ``Induction n``. That command failed because no such
-tactic exists (tactics are now in lowercase…), and the wrong word is
-underlined.
+tactic exists (names of standard tactics are written in lowercase),
+and the failing command is underlined.
 
 Notice that the processed part of the running buffer is not editable. If
 you ever want to modify something you have to go backward using the up
@@ -82,8 +82,8 @@ background in the error background color (pink by default). The same
 characterization of error-handling applies when running several commands using
 the "goto" button.
 
-If you ever try to execute a command which happens to run during a
-long time, and would like to abort it before its termination, you may
+If you ever try to execute a command that runs for a long time
+and would like to abort it before it terminates, you may
 use the interrupt button (the white cross on a red circle).
 
 There are other buttons on the |CoqIDE| toolbar: a button to save the running
@@ -141,11 +141,10 @@ Vernacular commands, templates
 
 The Templates menu allows using shortcuts to insert vernacular
 commands. This is a nice way to proceed if you are not sure of the
-spelling of the command you want.
+syntax of the command you want.
 
-Moreover, this menu offers some *templates* which will automatic
-insert a complex command like ``Fixpoint`` with a convenient shape for its
-arguments.
+Moreover, from this menu you can automatically insert templates of complex
+commands like ``Fixpoint`` that you can conveniently fill afterwards.
 
 Queries
 ------------
@@ -177,7 +176,7 @@ The `Compile` menu offers direct commands to:
 Customizations
 -------------------
 
-You may customize your environment using menu Edit/Preferences. A new
+You may customize your environment using the menu Edit/Preferences. A new
 window will be displayed, with several customization sections
 presented as a notebook.
 
@@ -189,7 +188,7 @@ automatic saving of files, by periodically saving the contents into
 files named `#f#` for each opened file `f`. You may also activate the
 *revert* feature: in case a opened file is modified on the disk by a
 third party, |CoqIDE| may read it again for you. Note that in the case
-you edited that same file, you will be prompt to choose to either
+you edited that same file, you will be prompted to choose to either
 discard your changes or not. The File charset encoding choice is
 described below in :ref:`character-encoding-saved-files`.
 
@@ -209,7 +208,7 @@ Notice that these settings are saved in the file `.coqiderc` of your
 home directory.
 
 A Gtk2 accelerator keymap is saved under the name `.coqide.keys`. It
-is not recommanded to edit this file manually: to modify a given menu
+is not recommended to edit this file manually: to modify a given menu
 shortcut, go to the corresponding menu item without releasing the
 mouse button, press the key you want for the new shortcut, and release
 the mouse button afterwards. If your system does not allow it, you may
@@ -240,14 +239,14 @@ mathematical symbols ∀ and ∃, you may define:
 
 There exists a small set of such notations already defined, in the
 file `utf8.v` of Coq library, so you may enable them just by
-``Require utf8`` inside |CoqIDE|, or equivalently, by starting |CoqIDE| with
-``coqide -l utf8``.
+``Require Import Unicode.Utf8`` inside |CoqIDE|, or equivalently,
+by starting |CoqIDE| with ``coqide -l utf8``.
 
 However, there are some issues when using such Unicode symbols: you of
 course need to use a character font which supports them. In the Fonts
 section of the preferences, the Preview line displays some Unicode
 symbols, so you could figure out if the selected font is OK. Related
-to this, one thing you may need to do is choose whether GTK+ should
+to this, one thing you may need to do is choosing whether GTK+ should
 use antialiased fonts or not, by setting the environment variable
 `GDK_USE_XFT` to 1 or 0 respectively.
 
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index e15bcb8e2c..973e1ccaac 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -434,7 +434,7 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use
 
   For users of coq_makefile with version < 8.7
 
-  + Support for “sub-directory” is deprecated. To perform actions before
+  + Support for "subdirectory" is deprecated. To perform actions before
     or after the build (like invoking ``make`` on a subdirectory) one can hook
     in pre-all and post-all extension points.
   + ``-extra-phony`` and ``-extra`` are deprecated. To provide additional target
@@ -442,10 +442,10 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use
 
 
 
-Modules dependencies
+Module dependencies
 --------------------
 
-In order to compute modules dependencies (so to use ``make``), |Coq| comes
+In order to compute module dependencies (so to use ``make``), |Coq| comes
 with an appropriate tool, ``coqdep``.
 
 ``coqdep`` computes inter-module dependencies for |Coq| and |OCaml|
@@ -460,7 +460,7 @@ command ``Declare ML Module``.
 Dependencies of |OCaml| modules are computed by looking at
 `open` commands and the dot notation *module.value*. However, this is
 done approximately and you are advised to use ``ocamldep`` instead for the
-|OCaml| modules dependencies.
+|OCaml| module dependencies.
 
 See the man page of ``coqdep`` for more details and options.
 
@@ -478,9 +478,9 @@ coqdoc is a documentation tool for the proof assistant |Coq|, similar to
 ``javadoc`` or ``ocamldoc``. The task of coqdoc is
 
 
-#. to produce a nice |Latex| and/or HTML document from the |Coq|
-   sources, readable for a human and not only for the proof assistant;
-#. to help the user navigating in his own (or third-party) sources.
+#. to produce a nice |Latex| and/or HTML document from |Coq| source files,
+   readable for a human and not only for the proof assistant;
+#. to help the user navigate his own (or third-party) sources.
 
 
 
@@ -491,7 +491,7 @@ Documentation is inserted into |Coq| files as *special comments*. Thus
 your files will compile as usual, whether you use coqdoc or not. coqdoc
 presupposes that the given |Coq| files are well-formed (at least
 lexically). Documentation starts with ``(**``, followed by a space, and
-ends with the pending ``*)``. The documentation format is inspired by Todd
+ends with ``*)``. The documentation format is inspired by Todd
 A. Coram’s *Almost Free Text (AFT)* tool: it is mainly ``ASCII`` text with
 some syntax-light controls, described below. coqdoc is robust: it
 shouldn’t fail, whatever the input is. But remember: “garbage in,
@@ -507,7 +507,7 @@ quoted code (thus you can quote a term like ``fun x => u`` by writing  ``[fun
 x => u]``). Inside quotations, the code is pretty-printed in the same
 way as it is in code parts.
 
-Pre-formatted vernacular is enclosed by ``[[`` and ``]]``. The former must be
+Preformatted vernacular is enclosed by ``[[`` and ``]]``. The former must be
 followed by a newline and the latter must follow a newline.
 
 
@@ -533,7 +533,7 @@ or
 
 
 It gives the |Latex| and HTML texts to be produced for the given |Coq|
-token. One of the |Latex| or HTML text may be omitted, causing the
+token. Either the |Latex| or the HTML rule may be omitted, causing the
 default pretty-printing to be used for this token.
 
 The printing for one token can be removed with
@@ -573,10 +573,9 @@ commands.
 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
-sub-section, etc. The section title is given on the remaining of the
-line.
+Sections are introduced by 1 to 4 asterisks at the beginning of a line
+followed by a space and the title of the section. One asterisk is a section,
+two a subsection, etc.
 
 .. example::
 
@@ -624,7 +623,7 @@ More than 4 leading dashes produce a horizontal rule.
 Emphasis.
 +++++++++
 
-Text can be italicized by placing it in underscores. A non-identifier
+Text can be italicized by enclosing it in underscores. A non-identifier
 character must precede the leading underscore and follow the trailing
 underscore, so that uses of underscores in names aren’t mistaken for
 emphasis. Usually, these are spaces or punctuation.
@@ -679,16 +678,16 @@ Hyperlinks can be inserted into the HTML output, so that any
 identifier is linked to the place of its definition.
 
 ``coqc file.v`` automatically dumps localization information in
-``file.glob`` or appends it to a file specified using option ``--dump-glob
+``file.glob`` or appends it to a file specified using the option ``--dump-glob
 file``. Take care of erasing this global file, if any, when starting
 the whole compilation process.
 
 Then invoke coqdoc or ``coqdoc --glob-from file`` to tell coqdoc to look
-for name resolutions into the file ``file`` (it will look in ``file.glob``
+for name resolutions in the file ``file`` (it will look in ``file.glob``
 by default).
 
-Identifiers from the |Coq| standard library are linked to the Coq web
-site at `<http://coq.inria.fr/library/>`_. This behavior can be changed
+Identifiers from the |Coq| standard library are linked to the Coq website
+`<http://coq.inria.fr/library/>`_. This behavior can be changed
 using command line options ``--no-externals`` and ``--coqlib``; see below.
 
 
@@ -731,12 +730,12 @@ file (even if it starts with a ``-``). |Coq| files are identified by the
 suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``.
 
 
-:HTML output: This is the default output. One HTML file is created for
+:HTML output: This is the default output format. One HTML file is created for
   each |Coq| file given on the command line, together with a file
   ``index.html`` (unless ``option-no-index is passed``). The HTML pages use a
   style sheet named ``style.css``. Such a file is distributed with coqdoc.
 :|Latex| output: A single |Latex| file is created, on standard
-  output. It can be redirected to a file with option ``-o``. The order of
+  output. It can be redirected to a file using the option ``-o``. The order of
   files on the command line is kept in the final document. |Latex|
   files given on the command line are copied ‘as is’ in the final
   document . DVI and PostScript can be produced directly with the
@@ -762,15 +761,15 @@ Command line options
   :-o file, --output file: Redirect the output into the file ‘file’
     (meaningless with ``-html``).
   :-d dir, --directory dir: Output files into directory ‘dir’ instead of
-    current directory (option ``-d`` does not change the filename specified
-    with option ``-o``, if any).
+    the current directory (option ``-d`` does not change the filename specified
+    with the option ``-o``, if any).
   :--body-only: Suppress the header and trailer of the final document.
     Thus, you can insert the resulting document into a larger one.
   :-p string, --preamble string: Insert some material in the |Latex|
     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 process in file ‘file’ as if
+  :--files-from file: Read file names 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.
@@ -781,7 +780,7 @@ Command line options
 
 **Index options**
 
-  Default behavior is to build an index, for the HTML output only,
+  The default behavior is to build an index, for the HTML output only,
   into ``index.html``.
 
   :--no-index: Do not output the index.
@@ -802,7 +801,7 @@ Command line options
     contents.
 
 
-**Hyperlinks options**
+**Hyperlink options**
 
   :--glob-from file: Make references using |Coq| globalizations from file
     file. (Such globalizations are obtained with Coq option ``-dump-glob``).
@@ -858,9 +857,9 @@ Command line options
     The behavior of options ``-g`` and ``-l`` can be locally overridden using the
     ``(* begin show *) … (* end show *)`` environment (see above).
 
-    There are a few options to drive the parsing of comments:
+    There are a few options that control the parsing of comments:
 
-  :--parse-comments: Parses regular comments delimited by ``(*`` and ``*)`` as
+  :--parse-comments: Parse regular comments delimited by ``(*`` and ``*)`` as
     well. They are typeset inline.
   :--plain-comments: Do not interpret comments, simply copy them as
     plain-text.
@@ -870,7 +869,7 @@ Command line options
 **Language options**
 
 
-  Default behavior is to assume ASCII 7 bits input files.
+  The default behavior is to assume ASCII 7 bit input files.
 
   :-latin1, --latin1: Select ISO-8859-1 input files. It is equivalent to
     --inputenc latin1 --charset iso-8859-1.
@@ -935,7 +934,7 @@ macros:
 Embedded Coq phrases inside |Latex| documents
 ---------------------------------------------
 
-When writing a documentation about a proof development, one may want
+When writing documentation about a proof development, one may want
 to insert |Coq| phrases inside a |Latex| document, possibly together
 with the corresponding answers of the system. We provide a mechanical
 way to process such |Coq| phrases embedded in |Latex| files: the ``coq-tex``