documentation fixes

document « Property »

more documentation fixes

[doc] destructed → destructured

[doc] another le_minus→lt_1_r

[doc] @jfehrle suggestions

[doc] more minor fixes

3 files changed, 41 insertions, 41 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 362c3da6cb..79eddbd3b5 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -368,7 +368,7 @@ We can check if a tactic made progress with:
    :name: progress
 
    :n:`@ltac_expr` is evaluated to v which must be a tactic value. The tactic value ``v``
-   is applied to each focued subgoal independently. If the application of ``v``
+   is applied to each focused subgoal independently. If the application of ``v``
    to one of the focused subgoal produced subgoals equal to the initial
    goals (up to syntactical equality), then an error of level 0 is raised.
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index ed980bd4de..1d08001e34 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -514,7 +514,7 @@ is a valid tactic expression.
 The pose tactic is also improved for the local definition of higher
 order terms. Local definitions of functions can use the same syntax as
 global ones.
-For example, the tactic :tacn:`pose <pose (ssreflect)>` supoprts parameters:
+For example, the tactic :tacn:`pose <pose (ssreflect)>` supports parameters:
 
 .. example::
 
@@ -684,7 +684,7 @@ conditions:
 + If this head is a projection of a canonical structure, then
   canonical structure equations are used for the matching.
 + If the head of term is *not* a constant, the subterm should have the
-  same structure (λ abstraction,let…in structure …).
+  same structure (λ abstraction, let…in structure …).
 + If the head of :token:`term` is a hole, the subterm should have at least as
   many arguments as :token:`term`.
 
@@ -1151,7 +1151,7 @@ is basically equivalent to
    move: a H1 H2; tactic => a H1 H2.
 
 
-with two differences: the in tactical will preserve the body of a ifa
+with two differences: the in tactical will preserve the body of an if a
 is a defined constant, and if the ``*`` is omitted it will use a
 temporary abbreviation to hide the statement of the goal from
 ``tactic``.
@@ -1706,7 +1706,7 @@ Intro patterns
   execution of tactic should thus generate exactly m subgoals, unless the
   ``[…]`` :token:`i_pattern` comes after an initial ``//`` or ``//=``
   :token:`s_item` that closes some of the goals produced by ``tactic``, in
-  which case exactly m subgoals should remain after thes- item, or we have
+  which case exactly m subgoals should remain after the :token:`s_item`, or we have
   the trivial branching :token:`i_pattern` [], which always does nothing,
   regardless of the number of remaining subgoals.
 ``[`` :token:`i_item` * ``| … |`` :token:`i_item` * ``]``
@@ -2240,8 +2240,8 @@ then the tactic
 
    tactic ; last k [ tactic1 |…| tacticm ] || tacticn.
 
-where natural denotes the integer k as above, applies tactic1 to the n
-−k + 1-th goal, … tacticm to the n −k + 2 − m-th goal and tactic n
+where natural denotes the integer :math:`k` as above, applies tactic1 to the
+:math:`n−k+1`\-th goal, … tacticm to the :math:`n−k+2`\-th goal and tacticn
 to the others.
 
 .. example::
@@ -2631,7 +2631,7 @@ The :token:`i_item` and :token:`s_item` can be used to interpret the asserted
 hypothesis with views (see section :ref:`views_and_reflection_ssr`) or simplify the resulting
 goals.
 
-The ``have`` tactic also supports a ``suff`` modifier which allows for
+The :tacn:`have` tactic also supports a ``suff`` modifier which allows for
 asserting that a given statement implies the current goal without
 copying the goal itself.
 
@@ -2651,7 +2651,7 @@ compatible with the presence of a list of binders.
 Generating let in context entries with have
 ```````````````````````````````````````````
 
-Since |SSR| 1.5 the ``have`` tactic supports a “transparent” modifier
+Since |SSR| 1.5 the :tacn:`have` tactic supports a “transparent” modifier
 to generate let in context entries: the ``@`` symbol in front of the
 context entry name.
 
@@ -2670,7 +2670,7 @@ context entry name.
      Lemma test n m (H : m + 1 < n) : True.
      have @i : 'I_n by apply: (Sub m); omega.
 
-Note that the sub-term produced by ``omega`` is in general huge and
+Note that the sub-term produced by :tacn:`omega` is in general huge and
 uninteresting, and hence one may want to hide it.
 For this purpose the ``[: name ]`` intro pattern and the tactic
 ``abstract`` (see :ref:`abstract_ssr`) are provided.
@@ -2782,7 +2782,7 @@ The
 ``have`` and ``suff`` tactics are equivalent and have the same syntax but:
 
 
-+ the order of the generated subgoals is inversed
++ the order of the generated subgoals is inverted
 + the optional clear item is still performed in the *second*
   branch. This means that the tactic:
 
@@ -5451,7 +5451,7 @@ equivalences are indeed taken into account, otherwise only single
    name of an open module. This command returns the list of lemmas:
 
    + whose *conclusion* contains a subterm matching the optional first
-     pattern. A - reverses the test, producing the list of lemmas whose
+     pattern. A ``-`` reverses the test, producing the list of lemmas whose
      conclusion does not contain any subterm matching the pattern;
    + whose name contains the given string. A ``-`` prefix reverses the test,
      producing the list of lemmas whose name does not contain the string. A
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index c910136406..78753fc053 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -157,10 +157,10 @@ The :n:`eqn:` construct in various tactics uses :n:`@naming_intropattern`.
 
 Use these elementary patterns to specify a name:
 
-* :n:`@ident` - use the specified name
-* :n:`?` - let Coq choose a name
-* :n:`?@ident` - generate a name that begins with :n:`@ident`
-* :n:`_` - discard the matched part (unless it is required for another
+* :n:`@ident` — use the specified name
+* :n:`?` — let Coq choose a name
+* :n:`?@ident` — generate a name that begins with :n:`@ident`
+* :n:`_` — discard the matched part (unless it is required for another
   hypothesis)
 * if a disjunction pattern omits a name, such as :g:`[|H2]`, Coq will choose a name
 
@@ -186,7 +186,7 @@ use the :tacn:`split` tactic to replace the current goal with subgoals :g:`A` an
 For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A`, or
 :tacn:`right` to replace the current goal with :g:`B`.
 
-* :n:`( {+, @simple_intropattern}` ) - matches
+* :n:`( {+, @simple_intropattern}` ) — matches
   a product over an inductive type with a
   :ref:`single constructor <intropattern_cons_note>`.
   If the number of patterns
@@ -196,7 +196,7 @@ For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A`
   If the number of patterns equals the number of constructor arguments plus the number
   of :n:`let-ins`, the patterns are applied to the arguments and :n:`let-in` variables.
 
-* :n:`( {+& @simple_intropattern} )` - matches a right-hand nested term that consists
+* :n:`( {+& @simple_intropattern} )` — matches a right-hand nested term that consists
   of one or more nested binary inductive types such as :g:`a1 OP1 a2 OP2 ...`
   (where the :g:`OPn` are right-associative).
   (If the :g:`OPn` are left-associative, additional parentheses will be needed to make the
@@ -207,15 +207,15 @@ For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A`
   :ref:`single constructor with two parameters <intropattern_cons_note>`.
   :ref:`Example <intropattern_ampersand_ex>`
 
-* :n:`[ {+| @intropattern_list} ]` - splits an inductive type that has
+* :n:`[ {+| @intropattern_list} ]` — splits an inductive type that has
   :ref:`multiple constructors <intropattern_cons_note>`
   such as :n:`A \/ B`
   into multiple subgoals.  The number of :token:`intropattern_list` must be the same as the number of
   constructors for the matched part.
-* :n:`[ {+ @intropattern} ]` - splits an inductive type that has a
+* :n:`[ {+ @intropattern} ]` — splits an inductive type that has a
   :ref:`single constructor with multiple parameters <intropattern_cons_note>`
   such as :n:`A /\ B` into multiple hypotheses.  Use :n:`[H1 [H2 H3]]` to match :g:`A /\ B /\ C`.
-* :n:`[]` - splits an inductive type:  If the inductive
+* :n:`[]` — splits an inductive type:  If the inductive
   type has multiple constructors, such as :n:`A \/ B`,
   create one subgoal for each constructor.  If the inductive type has a single constructor with
   multiple parameters, such as :n:`A /\ B`, split it into multiple hypotheses.
@@ -224,14 +224,14 @@ For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A`
 
 These patterns can be used when the hypothesis is an equality:
 
-* :n:`->` - replaces the right-hand side of the hypothesis with the left-hand
+* :n:`->` — replaces the right-hand side of the hypothesis with the left-hand
   side of the hypothesis in the conclusion of the goal; the hypothesis is
   cleared; if the left-hand side of the hypothesis is a variable, it is
   substituted everywhere in the context and the variable is removed.
   :ref:`Example <intropattern_rarrow_ex>`
-* :n:`<-` - similar to :n:`->`, but replaces the left-hand side of the hypothesis
+* :n:`<-` — similar to :n:`->`, but replaces the left-hand side of the hypothesis
   with the right-hand side of the hypothesis.
-* :n:`[= {*, @intropattern} ]` - If the product is over an equality type,
+* :n:`[= {*, @intropattern} ]` — If the product is over an equality type,
   applies either :tacn:`injection` or :tacn:`discriminate`.
   If :tacn:`injection` is applicable, the intropattern
   is used on the hypotheses generated by :tacn:`injection`.  If the
@@ -241,16 +241,16 @@ These patterns can be used when the hypothesis is an equality:
 
 **Other patterns**
 
-* :n:`*` - introduces one or more quantified variables from the result
+* :n:`*` — introduces one or more quantified variables from the result
   until there are no more quantified variables.
   :ref:`Example <intropattern_star_ex>`
 
-* :n:`**` - introduces one or more quantified variables or hypotheses from the result until there are
+* :n:`**` — introduces one or more quantified variables or hypotheses from the result until there are
   no more quantified variables or implications (:g:`->`).  :g:`intros **` is equivalent
   to :g:`intros`.
   :ref:`Example <intropattern_2stars_ex>`
 
-* :n:`@simple_intropattern_closed {* % @term}` - first applies each of the terms
+* :n:`@simple_intropattern_closed {* % @term}` — first applies each of the terms
   with the :tacn:`apply ... in` tactic on the hypothesis to be introduced, then it uses
   :n:`@simple_intropattern_closed`.
   :ref:`Example <intropattern_injection_ex>`
@@ -1409,7 +1409,7 @@ Controlling the proof flow
 
    While the different variants of :tacn:`assert` expect that no existential
    variables are generated by the tactic, :tacn:`eassert` removes this constraint.
-   This allows not to specify the asserted statement completeley before starting
+   This lets you avoid specifying the asserted statement completely before starting
    to prove it.
 
 .. tacv:: pose proof @term {? as @simple_intropattern}
@@ -1555,8 +1555,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
    :name: instantiate
 
    The instantiate tactic refines (see :tacn:`refine`) an existential variable
-   :n:`@ident` with the term :n:`@term`. It is equivalent to only [ident]:
-   :n:`refine @term` (preferred alternative).
+   :n:`@ident` with the term :n:`@term`. It is equivalent to
+   :n:`only [ident]: refine @term` (preferred alternative).
 
    .. note:: To be able to refer to an existential variable by name, the user
              must have given the name explicitly (see :ref:`Existential-Variables`).
@@ -2008,7 +2008,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
 
    .. coqtop:: reset all
 
-      Lemma le_minus : forall n:nat, n < 1 -> n = 0.
+      Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.
       intros n H ; induction H.
 
    Here we did not get any information on the indexes to help fulfill
@@ -2020,7 +2020,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    .. coqtop:: reset all
 
       Require Import Coq.Program.Equality.
-      Lemma le_minus : forall n:nat, n < 1 -> n = 0.
+      Lemma lt_1_r : forall n:nat, n < 1 -> n = 0.
       intros n H ; dependent induction H.
 
    The subgoal is cleaned up as the tactic tries to automatically
@@ -2691,7 +2691,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
 
    This tactic applies to any goal. The type of :token:`term` must have the form
 
-   ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``). eq term``:sub:`1` ``term``:sub:`2` ``.``
+   ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``), eq term``:sub:`1` ``term``:sub:`2` ``.``
 
    where :g:`eq` is the Leibniz equality or a registered setoid equality.
 
@@ -3224,8 +3224,8 @@ the conversion in hypotheses :n:`{+ @ident}`.
      even if an extra simplification is possible.
 
    In detail, the tactic :tacn:`simpl` first applies :math:`\beta`:math:`\iota`-reduction. Then, it
-   expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`-
-   reduction. But, when no :math:`\iota` rule is applied after unfolding then
+   expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`-reduction.
+   But, when no :math:`\iota` rule is applied after unfolding then
    :math:`\delta`-reductions are not applied. For instance trying to use :tacn:`simpl` on
    :g:`(plus n O) = n` changes nothing.
 
@@ -4005,8 +4005,8 @@ use one or several databases specific to your development.
 
    This vernacular command adds the terms :n:`{+ @term}` (their types must be
    equalities) in the rewriting bases :n:`{+ @ident}` with the default orientation
-   (left to right). Notice that the rewriting bases are distinct from the ``auto``
-   hint bases and thatauto does not take them into account.
+   (left to right). Notice that the rewriting bases are distinct from the :tacn:`auto`
+   hint bases and that :tacn:`auto` does not take them into account.
 
    This command is synchronous with the section mechanism (see :ref:`section-mechanism`):
    when closing a section, all aliases created by ``Hint Rewrite`` in that
@@ -4553,7 +4553,7 @@ Inversion
 
    .. tacv:: functional inversion @num
 
-      This does the same thing as :n:`intros until @num` folowed by
+      This does the same thing as :n:`intros until @num` followed by
       :n:`functional inversion @ident` where :token:`ident` is the
       identifier for the last introduced hypothesis.
 
@@ -4569,8 +4569,8 @@ Inversion
 Classical tactics
 -----------------
 
-In order to ease the proving process, when the Classical module is
-loaded. A few more tactics are available. Make sure to load the module
+In order to ease the proving process, when the ``Classical`` module is
+loaded, a few more tactics are available. Make sure to load the module
 using the ``Require Import`` command.
 
 .. tacn:: classical_left
@@ -4627,7 +4627,7 @@ Automating
 
    The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision
    procedure for Presburger arithmetic. It solves quantifier-free
-   formulas built with `~`, `\/`, `/\`, `->` on top of equalities,
+   formulas built with `~`, `\\/`, `/\\`, `->` on top of equalities,
    inequalities and disequalities on both the type :g:`nat` of natural numbers
    and :g:`Z` of binary integers. This tactic must be loaded by the command
    ``Require Import Omega``. See the additional documentation about omega