documentation fixes

document « Property »

more documentation fixes

[doc] destructed → destructured

[doc] another le_minus→lt_1_r

[doc] @jfehrle suggestions

[doc] more minor fixes

8 files changed, 63 insertions, 64 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 1611e9dd52..c08a9ed0e6 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1147,7 +1147,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or
    Polymorphism`.
 
    An inductive type can be forced to be template polymorphic using the
-   ``template`` attribute: it should then fullfill the criterion to
+   ``template`` attribute: it should then fulfill the criterion to
    be template polymorphic or an error is raised.
 
 .. exn:: Inductive @ident cannot be made template polymorphic.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 2d047a1058..f477bf239d 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -182,7 +182,7 @@ other arguments are the parameters of the inductive type.
    recursive (references to the record's name in the type of its field
    raises an  error). To define recursive records, one can use the ``Inductive``
    and ``CoInductive`` keywords, resulting in an inductive or co-inductive record.
-   Definition of mutal inductive or co-inductive records are also allowed, as long
+   Definition of mutually inductive or co-inductive records are also allowed, as long
    as all of the types in the block are records.
 
 .. note:: Induction schemes are automatically generated for inductive records.
@@ -1415,7 +1415,7 @@ is needed. In this translation, names in the file system are called
 *physical* paths while |Coq| names are contrastingly called *logical*
 names.
 
-A logical prefix Lib can be associated to a physical pathpath using
+A logical prefix Lib can be associated with a physical path using
 the command line option ``-Q`` `path` ``Lib``. All subfolders of path are
 recursively associated to the logical path ``Lib`` extended with the
 corresponding suffix coming from the physical path. For instance, the
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 2cbd41af8b..ae9d284661 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -111,7 +111,7 @@ Other tokens
   tokens defined at any given time can vary because the :cmd:`Notation`
   command can define new tokens.  A :cmd:`Require` command may load more notation definitions,
   while the end of a :cmd:`Section` may remove notations.  Some notations
-  are defined in the basic library (see :ref:`thecoqlibrary`) and are normallly
+  are defined in the basic library (see :ref:`thecoqlibrary`) and are normally
   loaded automatically at startup time.
 
   Here are the character sequences that Coq directly defines as tokens
@@ -395,7 +395,7 @@ stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
 Definition by case analysis
 ---------------------------
 
-Objects of inductive types can be destructurated by a case-analysis
+Objects of inductive types can be destructured by a case-analysis
 construction called *pattern matching* expression. A pattern matching
 expression is used to analyze the structure of an inductive object and
 to apply specific treatments accordingly.
@@ -572,7 +572,7 @@ The Vernacular
    assertion          : `assertion_keyword` `ident` [`binders`] : `term` .
    assertion_keyword  : Theorem | Lemma
                       : Remark | Fact
-                      : Corollary | Proposition
+                      : Corollary | Property | Proposition
                       : Definition | Example
    proof              : Proof . … Qed .
                       : Proof . … Defined .
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 9e219bd503..e5edd08995 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -359,7 +359,7 @@ line timing data:
     pass  ``TIMING=before`` or ``TIMING=after`` rather than ``TIMING=1``.
 
     .. note::
-       The sorting used here is the same as in the ``print-pretty-timed -diff`` target.
+       The sorting used here is the same as in the ``print-pretty-timed-diff`` target.
 
     .. note::
        This target requires python to build the table.
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
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index fd315c097d..bcc5e914ac 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -267,31 +267,30 @@ The second, more powerful control on printing is by using the format
 A *format* is an extension of the string denoting the notation with
 the possible following elements delimited by single quotes:
 
-- extra spaces are translated into simple spaces
+- tokens of the form ``'/ '`` are translated into breaking points.  If
+  there is a line break, indents the number of spaces appearing after the
+  “``/``” (no indentation in the example)
 
-- tokens of the form ``'/ '`` are translated into breaking point, in
-  case a line break occurs, an indentation of the number of spaces after
-  the “ ``/``” is applied (2 spaces in the given example)
-
-- token of the form ``'//'`` force writing on a new line
+- tokens of the form ``'//'`` force writing on a new line
 
 - well-bracketed pairs of tokens of the form ``'[ '`` and ``']'`` are
-  translated into printing boxes; in case a line break occurs, an extra
-  indentation of the number of spaces given after the “ ``[``” is applied
-  (4 spaces in the example)
+  translated into printing boxes; if there is a line break, an extra
+  indentation of the number of spaces after the “``[``” is applied
 
 - well-bracketed pairs of tokens of the form ``'[hv '`` and ``']'`` are
   translated into horizontal-or-else-vertical printing boxes; if the
   content of the box does not fit on a single line, then every breaking
-  point forces a newline and an extra indentation of the number of
-  spaces given after the “ ``[``” is applied at the beginning of each
-  newline (3 spaces in the example)
+  point forces a new line and an extra indentation of the number of
+  spaces after the “``[hv``” is applied at the beginning of each new line
 
 - well-bracketed pairs of tokens of the form ``'[v '`` and ``']'`` are
   translated into vertical printing boxes; every breaking point forces a
-  newline, even if the line is large enough to display the whole content
-  of the box, and an extra indentation of the number of spaces given
-  after the “``[``” is applied at the beginning of each newline
+  new line, even if the line is large enough to display the whole content
+  of the box, and an extra indentation of the number of spaces
+  after the “``[v``” is applied at the beginning of each new line (3 spaces
+  in the example)
+
+- extra spaces in other tokens are preserved in the output
 
 Notations disappear when a section is closed. No typing of the denoted
 expression is performed at definition time. Type checking is done only
@@ -592,7 +591,7 @@ placeholder being the nesting point. In the innermost occurrence of the
 nested iterating pattern, the second placeholder is finally filled with the
 terminating expression.
 
-In the example above, the iterator :math:`φ([~]_E , [~]_I)` is :math:`cons [~]_E [~]_I`
+In the example above, the iterator :math:`φ([~]_E , [~]_I)` is :math:`cons [~]_E\, [~]_I`
 and the terminating expression is ``nil``. Here are other examples:
 
 .. coqtop:: in