Improved grammar and spelling in chapters 'Type Classes', 'Omega' and 'Micromega' of the Reference Manual.

3 files changed, 35 insertions, 40 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 2407a9051a..d03a31c044 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -20,7 +20,7 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``.
 + :tacn:`nra` is an incomplete proof procedure for non-linear (real or
   rational) arithmetic;
 + :tacn:`psatz` ``D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and
-  ``n`` is an optional integer limiting the proof search depth
+  ``n`` is an optional integer limiting the proof search depth,
   is an incomplete proof procedure for non-linear arithmetic.
   It is based on John Harrison’s HOL Light
   driver to the external prover `csdp` [#]_. Note that the `csdp` driver is
@@ -32,10 +32,10 @@ arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}.
 The syntax of the formulas is the following:
 
  .. productionlist:: `F`
-   F : A ∣ P ∣ True ∣ False ∣ F 1 ∧ F 2 ∣ F 1 ∨ F 2 ∣ F 1 ↔ F 2 ∣ F 1 → F 2 ∣ ¬ F
-   A : p 1 = p 2 ∣ p 1 > p 2 ∣ p 1 < p 2 ∣ p 1 ≥ p 2 ∣ p 1 ≤ p 2
-   p : c ∣ x ∣ −p ∣ p 1 − p 2 ∣ p 1 + p 2 ∣ p 1 × p 2 ∣ p ^ n
-		     
+   F : A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F
+   A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p
+   p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n
+
 where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the
 operators :math:`−, +, ×` are respectively subtraction, addition, and product;
 :math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition.
@@ -81,11 +81,11 @@ If :math:`-1` belongs to :math:`\mathit{Cone}(S)`, then the conjunction
 A proof based on this theorem is called a *positivstellensatz*
 refutation. The tactics work as follows. Formulas are normalized into
 conjunctive normal form :math:`\bigwedge_i C_i` where :math:`C_i` has the
-general form :math:`(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False})` and
+general form :math:`(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False}` and
 :math:`\Join \in \{>,\ge,=\}` for :math:`D\in \{\mathbb{Q},\mathbb{R}\}` and
 :math:`\Join \in \{\ge, =\}` for :math:`\mathbb{Z}`.
 
-For each conjunct :math:`C_i`, the tactic calls a oracle which searches for
+For each conjunct :math:`C_i`, the tactic calls an oracle which searches for
 :math:`-1` within the cone. Upon success, the oracle returns a *cone
 expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`)
 and checked to be :math:`-1`.
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 80ce016200..1ed3bffd2c 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -8,23 +8,20 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic
 Description of ``omega``
 ------------------------
 
-This tactic does not need any parameter:
-
 .. tacn:: omega
 
-:tacn:`omega` solves a goal in Presburger arithmetic, i.e. a universally
-quantified formula made of equations and inequations. Equations may
-be specified either on the type ``nat`` of natural numbers or on
-the type ``Z`` of binary-encoded integer numbers. Formulas on
-``nat`` are automatically injected into ``Z``.  The procedure
-may use any hypothesis of the current proof session to solve the goal.
+   :tacn:`omega` is a tactic for solving goals in Presburger arithmetic,
+   i.e. for proving formulas made of equations and inequations over the
+   type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers.
+   Formulas on ``nat`` are automatically injected into ``Z``. The procedure
+   may use any hypothesis of the current proof session to solve the goal.
 
-Multiplication is handled by :tacn:`omega` but only goals where at
-least one of the two multiplicands of products is a constant are
-solvable. This is the restriction meant by "Presburger arithmetic".
+   Multiplication is handled by :tacn:`omega` but only goals where at
+   least one of the two multiplicands of products is a constant are
+   solvable. This is the restriction meant by "Presburger arithmetic".
 
-If the tactic cannot solve the goal, it fails with an error message.
-In any case, the computation eventually stops.
+   If the tactic cannot solve the goal, it fails with an error message.
+   In any case, the computation eventually stops.
 
 .. tacv:: romega
    :name: romega
@@ -34,8 +31,7 @@ In any case, the computation eventually stops.
 Arithmetical goals recognized by ``omega``
 ------------------------------------------
 
-:tacn:`omega` applied only to quantifier-free formulas built from the
-connectors::
+:tacn:`omega` applies only to quantifier-free formulas built from the connectives::
 
    /\  \/  ~  ->
 
@@ -67,8 +63,8 @@ is generated:
   universally quantified, try :tacn:`intros` first; if it contains
   existentials quantifiers too, :tacn:`omega` is not strong enough to solve your
   goal). This may happen also if your goal contains arithmetical
-  operators unknown from :tacn:`omega`. Finally, your goal may be really
-  wrong!
+  operators not recognized by :tacn:`omega`. Finally, your goal may be simply
+  not true!
 
 .. exn:: omega: Not a quantifier-free goal.
 
@@ -145,10 +141,10 @@ Overview of the tactic
 ~~~~~~~~~~~~~~~~~~~~~~
 
  * The goal is negated twice and the first negation is introduced as an hypothesis.
- * Hypothesis are decomposed in simple equations or inequations. Multiple
+ * Hypotheses are decomposed in simple equations or inequations. Multiple
    goals may result from this phase.
  * Equations and inequations over ``nat`` are translated over
-   ``Z``, multiple goals may result from the translation of substraction.
+   ``Z``, multiple goals may result from the translation of subtraction.
  * Equations and inequations are normalized.
  * Goals are solved by the OMEGA decision procedure.
  * The script of the solution is replayed.
@@ -158,16 +154,15 @@ Overview of the OMEGA decision procedure
 
 The OMEGA decision procedure involved in the :tacn:`omega` tactic uses
 a small subset of the decision procedure presented in :cite:`TheOmegaPaper`
-Here is an overview, look at the original paper for more information.
+Here is an overview, refer to the original paper for more information.
 
  * Equations and inequations are normalized by division by the GCD of their
    coefficients.
  * Equations are eliminated, using the Banerjee test to get a coefficient
    equal to one.
- * Note that each inequation defines a half space in the space of real value
-   of the variables.
+ * Note that each inequation cuts the Euclidean space in half.
  * Inequations are solved by projecting on the hyperspace
-   defined by cancelling one of the variable.  They are partitioned
+   defined by cancelling one of the variables. They are partitioned
    according to the sign of the coefficient of the eliminated
    variable. Pairs of inequations from different classes define a
    new edge in the projection.
@@ -177,7 +172,7 @@ Here is an overview, look at the original paper for more information.
    (success) or there is no more variable to eliminate (failure).
 
 It may happen that there is a real solution and no integer one. The last
-steps of the Omega procedure (dark shadow) are not implemented, so the
+steps of the Omega procedure are not implemented, so the
 decision procedure is only partial.
 
 Bugs
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 68b5b9d6fe..b7946c6451 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -120,7 +120,7 @@ Following the previous example, one can write:
 
    Generalizable Variables A B C.
 
-   Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).
+   Definition neqb_implicit `{eqa : EqDec A} (x y : A) := negb (eqb x y).
 
 Here ``A`` is implicitly generalized, and the resulting function is
 equivalent to the one above.
@@ -193,7 +193,7 @@ superclasses as a binding context:
    Class Ord `(E : EqDec A) := { le : A -> A -> bool }.
 
 Contrary to Haskell, we have no special syntax for superclasses, but
-this declaration is morally equivalent to:
+this declaration is equivalent to:
 
 ::
 
@@ -248,7 +248,7 @@ properties, e.g.:
 
 This declares singleton classes for reflexive and transitive relations,
 (see the :ref:`singleton class <singleton-class>` variant for an
-explanation). These may be used as part of other classes:
+explanation). These may be used as parts of other classes:
 
 .. coqtop:: all
 
@@ -346,7 +346,7 @@ few other commands related to type classes.
 
 .. cmd:: Existing Instance {+ @ident} [| priority]
 
-   This commands adds an arbitrary list of constants whose type ends with
+   This command adds an arbitrary list of constants whose type ends with
    an applied type class to the instance database with an optional
    priority.  It can be used for redeclaring instances at the end of
    sections, or declaring structure projections as instances. This is
@@ -387,14 +387,14 @@ few other commands related to type classes.
 
    + When called with specific databases (e.g. with), typeclasses eauto
      allows shelved goals to remain at any point during search and treat
-     typeclasses goals like any other.
+     typeclass goals like any other.
 
    + The transparency information of databases is used consistently for
      all hints declared in them. It is always used when calling the
-     unifier. When considering the local hypotheses, we use the transparent
+     unifier. When considering local hypotheses, we use the transparent
      state of the first hint database given. Using an empty database
      (created with :cmd:`Create HintDb` for example) with unfoldable variables and
-     constants as the first argument of typeclasses eauto hence makes
+     constants as the first argument of ``typeclasses eauto`` hence makes
      resolution with the local hypotheses use full conversion during
      unification.
 
@@ -461,8 +461,8 @@ Options
 .. opt:: Typeclasses Dependency Order
 
    This option (on by default since 8.6) respects the dependency order
-   between subgoals, meaning that subgoals which are depended on by other
-   subgoals come first, while the non-dependent subgoals were put before
+   between subgoals, meaning that subgoals on which other subgoals depend
+   come first, while the non-dependent subgoals were put before
    the dependent ones previously (Coq 8.5 and below). This can result in
    quite different performance behaviors of proof search.