Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' and 'Tactics' of the Reference Manual.

3 files changed, 66 insertions, 57 deletions

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index eba0db3ff..44376080c 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -321,7 +321,7 @@ Navigation in the proof tree
    goal, much like :cmd:`Focus` does, however, the subproof can only be
    unfocused when it has been fully solved ( *i.e.* when there is no
    focused goal left). Unfocusing is then handled by ``}`` (again, without a
-   terminating period). See also example in next section.
+   terminating period). See also an example in the next section.
 
    Note that when a focused goal is proved a message is displayed
    together with a suggestion about the right bullet or ``}`` to unfocus it
@@ -403,7 +403,7 @@ The following example script illustrates all these features:
 
 .. exn:: No such goal. Focus next goal with bullet @bullet.
 
-   You tried to apply a tactic but no goal where under focus. Using :n:`@bullet` is  mandatory here.
+   You tried to apply a tactic but no goals were under focus. Using :n:`@bullet` is  mandatory here.
 
 .. exn:: No such goal. Try unfocusing with %{.
 
@@ -470,7 +470,7 @@ Requesting information
       constructed. These holes appear as a question mark indexed by an
       integer, and applied to the list of variables in the context, since it
       may depend on them. The types obtained by abstracting away the context
-      from the type of each hole-placer are also printed.
+      from the type of each placeholder are also printed.
 
    .. cmdv:: Show Conjectures
       :name: Show Conjectures
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 562f8568d..9b4d724e0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -26,8 +26,8 @@ address a particular goal in the list by writing n:tactic which means
 “apply tactic tactic to goal number n”. We can show the list of
 subgoals by typing Show (see Section :ref:`requestinginformation`).
 
-Since not every rule applies to a given statement, every tactic cannot
-be used to reduce any goal. In other words, before applying a tactic
+Since not every rule applies to a given statement, not every tactic can
+be used to reduce a given goal. In other words, before applying a tactic
 to a given goal, the system checks that some *preconditions* are
 satisfied. If it is not the case, the tactic raises an error message.
 
@@ -107,10 +107,10 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
 
 .. _occurencessets:
 
-Occurrences sets and occurrences clauses
+Occurrence sets and occurrence clauses
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-An occurrences clause is a modifier to some tactics that obeys the
+An occurrence clause is a modifier to some tactics that obeys the
 following syntax:
 
 .. _tactic_occurence_grammar:
@@ -137,7 +137,7 @@ negates the condition so that the clause denotes all the occurrences
 except the ones explicitly mentioned after the minus sign.
 
 As an exception to the left-to-right order, the occurrences in
-thereturn subexpression of a match are considered *before* the
+the return subexpression of a match are considered *before* the
 occurrences in the matched term.
 
 In the second case, the ``*`` on the left of ``|-`` means that all occurrences
@@ -151,7 +151,7 @@ no numbers are given, all occurrences of :n:`@term` in the goal are selected.
 Finally, the last notation is an abbreviation for ``* |- *``. Note also
 that ``|-`` is optional in the first case when no ``*`` is given.
 
-Here are some tactics that understand occurrences clauses: :tacn:`set`, :tacn:`remember`
+Here are some tactics that understand occurrence clauses: :tacn:`set`, :tacn:`remember`
 , :tacn:`induction`, :tacn:`destruct`.
 
 
@@ -466,7 +466,7 @@ Applying theorems
    the tuple is (recursively) decomposed and the first component of the tuple
    of which a non-dependent premise matches the conclusion of the type of
    :n:`@ident`. Tuples are decomposed in a width-first left-to-right order (for
-   instance if the type of :g:`H1` is a :g:`A <-> B` statement, and the type of
+   instance if the type of :g:`H1` is :g:`A <-> B` and the type of
    :g:`H2` is :g:`A` then ``apply H1 in H2`` transforms the type of :g:`H2`
    into :g:`B`). The tactic ``apply`` relies on first-order pattern-matching
    with dependent types.
@@ -846,7 +846,7 @@ quantification or an implication.
    :n:`intros {+ p}` is not equivalent to :n:`intros p; ... ; intros p`
    for the following reason: If one of the :n:`p` is a wildcard pattern, it
    might succeed in the first case because the further hypotheses it
-   depends in are eventually erased too while it might fail in the second
+   depends on are eventually erased too while it might fail in the second
    case because of dependencies in hypotheses which are not yet
    introduced (and a fortiori not yet erased).
 
@@ -1040,7 +1040,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
 .. tacv:: remember @term as @ident in @goal_occurrences
 
    This is a more general form of :n:`remember` that remembers the occurrences
-   of term specified by an occurrences set.
+   of term specified by an occurrence set.
 
 .. tacv:: eremember @term as @ident
 .. tacv:: eremember @term as @ident in @goal_occurrences
@@ -1523,7 +1523,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
 
 .. tacv:: case_eq @term
 
-   The tactic :n:`case_eq` is a variant of the :n:`case` tactic that allow to
+   The tactic :n:`case_eq` is a variant of the :n:`case` tactic that allows to
    perform case analysis on a term without completely forgetting its original
    form. This is done by generating equalities between the original form of the
    term and the outcomes of the case analysis.
@@ -1806,7 +1806,7 @@ and an explanation of the underlying technique.
    following the definition of a function. It makes use of a principle
    generated by ``Function`` (see :ref:`advanced-recursive-functions`) or
    ``Functional Scheme`` (see :ref:`functional-scheme`).
-   Note that this tactic is only available after a
+   Note that this tactic is only available after a ``Require Import FunInd``.
 
 .. example::
    .. coqtop:: reset all
@@ -1825,7 +1825,7 @@ and an explanation of the underlying technique.
    arguments explicitly.
 
 .. note::
-   Parentheses over :n:`@qualid {+ @term}` are mandatory.
+   Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped.
 
 .. note::
    :n:`functional induction (f x1 x2 x3)` is actually a wrapper for
@@ -2237,7 +2237,7 @@ See also: :ref:`advanced-recursive-functions`
 
    To prove the goal, we may need to reason by cases on H and to derive
    that m is necessarily of the form (S m 0 ) for certain m 0 and that
-   (Le n m 0 ). Deriving these conditions corresponds to prove that the
+   (Le n m 0 ). Deriving these conditions corresponds to proving that the
    only possible constructor of (Le (S n) m) isLeS and that we can invert
    the-> in the type of LeS. This inversion is possible because Le is the
    smallest set closed by the constructors LeO and LeS.
@@ -2598,7 +2598,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 
       Adds :n:`@term` to the database used by :tacn:`stepl`.
 
-   The tactic is especially useful for parametric setoids which are not accepted
+   This tactic is especially useful for parametric setoids which are not accepted
    as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
    :ref:`Generalizedrewriting`).
 
@@ -2708,7 +2708,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    Normalization according to the flags is done by first evaluating the
    head of the expression into a *weak-head* normal form, i.e. until the
-   evaluation is bloked by a variable (or an opaque constant, or an
+   evaluation is blocked by a variable (or an opaque constant, or an
    axiom), as e.g. in :g:`x u1 ... un` , or :g:`match x with ... end`, or
    :g:`(fix f x {struct x} := ...) x`, or is a constructed form (a
    :math:`\lambda`-expression, a constructor, a cofixpoint, an inductive type, a
@@ -2804,14 +2804,18 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    This tactic applies to a goal that has the form::
 
-     forall (x:T1) ... (xk:Tk), t
+     forall (x:T1) ... (xk:Tk), T
 
-   with :g:`t` :math:`\beta`:math:`\iota`:math:`\zeta`-reducing to :g:`c t`:sub:`1` :g:`... t`:sub:`n` and :g:`c` a
+   with :g:`T` :math:`\beta`:math:`\iota`:math:`\zeta`-reducing to :g:`c t`:sub:`1` :g:`... t`:sub:`n` and :g:`c` a
    constant. If :g:`c` is transparent then it replaces :g:`c` with its
    definition (say :g:`t`) and then reduces
    :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules.
 
 .. exn:: Not reducible.
+   :undocumented:
+
+.. exn:: No head constant to reduce.
+   :undocumented:
 
 .. tacn:: hnf
    :name: hnf
@@ -2821,8 +2825,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    reduces the head of the goal until it becomes a product or an
    irreducible term. All inner :math:`\beta`:math:`\iota`-redexes are also reduced.
 
-   Example: The term :g:`forall n:nat, (plus (S n) (S n))` is not reduced by
-   :n:`hnf`.
+   Example: The term :g:`fun n : nat => S n + S n` is not reduced by :n:`hnf`.
 
 .. note::
  The :math:`\delta` rule only applies to transparent constants (see :ref:`vernac-controlling-the-reduction-strategies`
@@ -2862,7 +2865,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    + A constant can be marked to be unfolded only if applied to enough
      arguments. The number of arguments required can be specified using the
-     ``/`` symbol in the arguments list of the ``Arguments`` vernacular command.
+     ``/`` symbol in the argument list of the :cmd:`Arguments` vernacular command.
 
      .. example::
         .. coqtop:: all
@@ -3030,7 +3033,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    For instance, if the current goal :g:`T` is expressible as
    :math:`\varphi`:g:`(t)` where the notation captures all the instances of :g:`t`
    in :math:`\varphi`:g:`(t)`, then :n:`pattern t` transforms it into
-   :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This command can be used, for
+   :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This tactic can be used, for
    instance, when the tactic ``apply`` fails on matching.
 
 .. tacv:: pattern @term at {+ @num}
@@ -3072,10 +3075,10 @@ Conversion tactics applied to hypotheses
    listed in this section.
 
    If :n:`@ident` is a local definition, then :n:`@ident` can be replaced by
-   (Type of :n:`@ident`) to address not the body but the type of the local
+   (type of :n:`@ident`) to address not the body but the type of the local
    definition.
 
-   Example: :n:`unfold not in (Type of H1) (Type of H3)`.
+   Example: :n:`unfold not in (type of H1) (type of H3)`.
 
 .. exn:: No such hypothesis: @ident.
 
@@ -3216,10 +3219,10 @@ in the given databases.
 .. tacn:: autorewrite with {+ @ident}
    :name: autorewrite
 
-This tactic [4]_ carries out rewritings according the rewriting rule
+This tactic [4]_ carries out rewritings according to the rewriting rule
 bases :n:`{+ @ident}`.
 
-Each rewriting rule of a base :n:`@ident` is applied to the main subgoal until
+Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until
 it fails. Once all the rules have been processed, if the main subgoal has
 progressed (e.g., if it is distinct from the initial main goal) then the rules
 of this base are processed again. If the main subgoal has not progressed then
@@ -3312,7 +3315,7 @@ automatically created.
    (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`),
    making the retrieval more efficient. The legacy implementation (the default one
    for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto`
-   goals), for non-Immediate hints and do not make use of transparency
+   goals), for non-Immediate hints and does not make use of transparency
    hints, putting more work on the unification that is run after
    retrieval (it keeps a list of the lemmas in case the DT is not used).
    The new implementation enabled by the discriminated option makes use
@@ -3496,7 +3499,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       The `emp` regexp does not match any search path while `eps`
       matches the empty path. During proof search, the path of
       successive successful hints on a search branch is recorded, as a
-      list of identifiers for the hints (note Hint Extern’s do not have
+      list of identifiers for the hints (note that Hint Extern’s do not have
       an associated identifier).
       Before applying any hint :n:`@ident` the current path `p` extended with
       :n:`@ident` is matched against the current cut expression `c` associated to
@@ -3535,15 +3538,14 @@ Hint databases defined in the Coq standard library
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Several hint databases are defined in the Coq standard library. The
-actual content of a database is the collection of the hints declared
+actual content of a database is the collection of hints declared
 to belong to this database in each of the various modules currently
-loaded. Especially, requiring new modules potentially extend a
-database. At Coq startup, only the core database is non empty and can
-be used.
+loaded. Especially, requiring new modules may extend the database.
+At Coq startup, only the core database is nonempty and can be used.
 
 :core: This special database is automatically used by ``auto``, except when
        pseudo-database ``nocore`` is given to ``auto``. The core database
-       contains only basic lemmas about negation, conjunction, and so on from.
+       contains only basic lemmas about negation, conjunction, and so on.
        Most of the hints in this database come from the Init and Logic directories.
 
 :arith: This database contains all lemmas about Peano’s arithmetic proved in the
@@ -3655,7 +3657,7 @@ but this is a mere workaround and has some limitations (for instance, external
 hints cannot be removed).
 
 A proper way to fix this issue is to bind the hints to their module scope, as
-for most of the other objects Coq uses. Hints should only made available when
+for most of the other objects Coq uses. Hints should only be made available when
 the module they are defined in is imported, not just required. It is very
 difficult to change the historical behavior, as it would break a lot of scripts.
 We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior`
@@ -3774,9 +3776,9 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary.
    :name: dtauto
 
    While :tacn:`tauto` recognizes inductively defined connectives isomorphic to
-   the standard connective ``and, prod, or, sum, False, Empty_set, unit, True``,
-   :tacn:`dtauto` recognizes also all inductive types with one constructors and
-   no indices, i.e. record-style connectives.
+   the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``,
+   ``Empty_set``, ``unit``, ``True``, :tacn:`dtauto` also recognizes all inductive
+   types with one constructor and no indices, i.e. record-style connectives.
 
 .. tacn:: intuition @tactic
    :name: intuition
@@ -3792,7 +3794,7 @@ For instance, the tactic :g:`intuition auto` applied to the goal
 
 ::
 
-    (forall (x:nat), P x)/\B -> (forall (y:nat),P y)/\ P O \/B/\ P O
+    (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O
 
 
 internally replaces it by the equivalent one:
@@ -3819,9 +3821,9 @@ some incompatibilities.
    :name: dintuition
 
    While :tacn:`intuition` recognizes inductively defined connectives
-   isomorphic to the standard connective ``and``, ``prod``, ``or``, ``sum``, ``False``,
-   ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` recognizes also all inductive
-   types with one constructors and no indices, i.e. record-style connectives.
+   isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``,
+   ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive
+   types with one constructor and no indices, i.e. record-style connectives.
 
 .. opt:: Intuition Negation Unfolding
 
@@ -3836,11 +3838,12 @@ The :tacn:`rtauto` tactic solves propositional tautologies similarly to what
 reflection scheme applied to a sequent calculus proof of the goal.  The search
 procedure is also implemented using a different technique.
 
-Users should be aware that this difference may result in faster proof- search
+Users should be aware that this difference may result in faster proof-search
 but slower proof-checking, and :tacn:`rtauto` might not solve goals that
 :tacn:`tauto` would be able to solve (e.g. goals involving universal
 quantifiers).
 
+Note that this tactic is only available after a ``Require Import Rtauto``.
 
 .. tacn:: firstorder
    :name: firstorder
@@ -3887,7 +3890,7 @@ inductive definition.
 
 The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard
 Nelson and Oppen congruence closure algorithm, which is a decision procedure
-for ground equalities with uninterpreted symbols. It also include the
+for ground equalities with uninterpreted symbols. It also includes
 constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal
 is a non-quantified equality, congruence tries to prove it with non-quantified
 equalities in the context. Otherwise it tries to infer a discriminable equality
@@ -3895,8 +3898,8 @@ from those in the context. Alternatively, congruence tries to prove that a
 hypothesis is equal to the goal or to the negation of another hypothesis.
 
 :tacn:`congruence` is also able to take advantage of hypotheses stating
-quantified equalities, you have to provide a bound for the number of extra
-equalities generated that way. Please note that one of the members of the
+quantified equalities, but you have to provide a bound for the number of extra
+equalities generated that way. Please note that one of the sides of the
 equality must contain all the quantified variables in order for congruence to
 match against it.
 
@@ -4071,10 +4074,10 @@ symbol :g:`=`.
 .. tacn:: decide equality
    :name: decide equality
 
-   This tactic solves a goal of the form :g:`forall x y:R, {x=y}+{ ~x=y}`,
+   This tactic solves a goal of the form :g:`forall x y : R, {x = y} + {~ x = y}`,
    where :g:`R` is an inductive type such that its constructors do not take
    proofs or functions as arguments, nor objects in dependent types. It
-   solves goals of the form :g:`{x=y}+{ ~x=y}` as well.
+   solves goals of the form :g:`{x = y} + {~ x = y}` as well.
 
 .. tacn:: compare @term @term
    :name: compare
@@ -4214,9 +4217,9 @@ using the ``Require Import`` command.
    Use ``classical_right`` to prove the right part of the disjunction with
    the assumption that the negation of left part holds.
 
-.. _tactics-automatizing:
+.. _tactics-automating:
 
-Automatizing
+Automating
 ------------
 
 
@@ -4245,6 +4248,12 @@ constructed over the following grammar:
   Internally, it uses a system very similar to the one of the ring
   tactic.
 
+  Note that this tactic is only available after a ``Require Import Btauto``.
+
+.. exn:: Cannot recognize a boolean equality.
+
+   The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto`
+   doesn't introduce variables into the context on its own.
 
 .. tacn:: omega
    :name: omega
@@ -4270,7 +4279,7 @@ distributivity, constant propagation) and comparing syntactically the
 results.
 
 :n:`ring_simplify` applies the normalization procedure described above to
-the terms given. The tactic then replaces all occurrences of the terms
+the given terms. The tactic then replaces all occurrences of the terms
 given in the conclusion of the goal by their normal forms. If no term
 is given, then the conclusion should be an equation and both hand
 sides are normalized.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index c37233734..0a517973c 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1097,7 +1097,7 @@ described first.
       The scope of :cmd:`Opaque` is limited to the current section, or current
       file, unless the variant :cmd:`Global Opaque` is used.
 
-   See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`,
+   See also: sections :ref:`performingcomputations`, :ref:`tactics-automating`,
    :ref:`proof-editing-mode`
 
    .. exn:: The reference @qualid was not found in the current environment.
@@ -1131,7 +1131,7 @@ described first.
       There is no constant referred by :n:`@qualid` in the environment.
 
    See also: sections :ref:`performingcomputations`,
-   :ref:`tactics-automatizing`, :ref:`proof-editing-mode`
+   :ref:`tactics-automating`, :ref:`proof-editing-mode`
 
 .. _vernac-strategy:
 
@@ -1217,19 +1217,19 @@ scope of their effect. There are four kinds of commands:
   current section or module it occurs in.  As an example, the :cmd:`Coercion`
   and :cmd:`Strategy` commands belong to this category.
 + Commands whose default behavior is to stop their effect at the end
-  of the section they occur in but to extent their effect outside the module or
+  of the section they occur in but to extend their effect outside the module or
   library file they occur in. For these commands, the Local modifier limits the
   effect of the command to the current module if the command does not occur in a
   section and the Global modifier extends the effect outside the current
   sections and current module if the command occurs in a section. As an example,
   the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong
   to this category. Notice that a subclass of these commands do not support
-  extension of their scope outside sections at all and the Global is not
+  extension of their scope outside sections at all and the Global modifier is not
   applicable to them.
 + Commands whose default behavior is to stop their effect at the end
   of the section or module they occur in.  For these commands, the ``Global``
   modifier extends their effect outside the sections and modules they
-  occurs in.  The :cmd:`Transparent` and :cmd:`Opaque`
+  occur in.  The :cmd:`Transparent` and :cmd:`Opaque`
   (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands
   belong to this category.
 + Commands whose default behavior is to extend their effect outside