Fixed a few wrong reference and typos

1 files changed, 14 insertions, 14 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index cc4976587d..fc08500613 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -487,7 +487,7 @@ used as a convenient shorthand for abstractions, especially in local
 definitions or type expressions.
 
 Wildcards may be interpreted as abstractions (see for example sections
-:ref:`definitions_ssr` and ref:`structure_ssr`), or their content can be
+:ref:`definitions_ssr` and :ref:`structure_ssr`), or their content can be
 inferred from the whole context of the goal (see for example section
 :ref:`abbreviations_ssr`).
 
@@ -983,13 +983,13 @@ During the course of a proof |Coq| always present the user with a
   Fk : Pk
   …
   =================
-  forall (xl : Tl ) …,
+  forall (xl : Tl) …,
   let ym := bm in … in
   Pn -> … -> C
 
 The *goal* to be proved appears below the double line; above the line
 is the *context* of the sequent, a set of declarations of *constants*
-``ci`` , *defined constants* d i , and *facts* ``Fk`` that can be used to
+``ci`` , *defined constants* ``dj`` , and *facts* ``Fk`` that can be used to
 prove the goal (usually, ``Ti`` , ``Tj : Type`` and ``Pk : Prop``).
 The various
 kinds of declarations can come in any order. The top part of the
@@ -1893,9 +1893,9 @@ under fresh |SSR| names.
       case E : a => H.
       Show 2.
 
-Combining the generation of named equations mechanism with thecase
+Combining the generation of named equations mechanism with the :tacn:`case`
 tactic strengthens the power of a case analysis. On the other hand,
-when combined with the elim tactic, this feature is mostly useful for
+when combined with the :tacn:`elim` tactic, this feature is mostly useful for
 debug purposes, to trace the values of decomposed parameters and
 pinpoint failing branches.
 
@@ -2022,7 +2022,7 @@ be substituted.
 
    The equation always refers to the first :token:`d_item` in the actual tactic
    call, before any padding with initial ``_``. Thus, if an inductive type
-   has two family parameters, it is possible to have|SSR| generate an
+   has two family parameters, it is possible to have |SSR| generate an
    equation for the second one by omitting the pattern for the first;
    note however that this will fail if the type of the second parameter
    depends on the value of the first parameter.
@@ -2320,7 +2320,7 @@ For instance, the tactic:
    tactic; do 1? rewrite mult_comm.
 
 rewrites at most one time the lemma ``mult_comm`` in all the subgoals
-generated by tactic , whereas the tactic:
+generated by tactic, whereas the tactic:
 
 .. coqdoc::
 
@@ -2511,7 +2511,7 @@ which behave like:
    have: term ; first by tactic.
    move=> clear_switch i_item.
 
-Note that the :token:`clear_switch` *precedes* the:token:`i_item`, which
+Note that the :token:`clear_switch` *precedes* the :token:`i_item`, which
 allows to reuse
 a name of the context, possibly used by the proof of the assumption,
 to introduce the new assumption itself.
@@ -2783,7 +2783,7 @@ The
 
 
 + the order of the generated subgoals is inversed
-+ but the optional clear item is still performed in the *second*
++ the optional clear item is still performed in the *second*
   branch. This means that the tactic:
 
   .. coqdoc::
@@ -2929,7 +2929,7 @@ facts.
 
 If an :token:`ident` is prefixed with the ``@`` mark, then a let-in redex is
 created, which keeps track if its body (if any). The syntax
-``( ident := c_pattern)`` allows to generalize an arbitrary term using a
+``(ident := c_pattern)`` allows to generalize an arbitrary term using a
 given name. Note that its simplest form ``(x := y)`` is just a renaming of
 ``y`` into ``x``. In particular, this can be useful in order to simulate the
 generalization of a section variable, otherwise not allowed. Indeed
@@ -3917,7 +3917,7 @@ definitely want to avoid repeating large subterms of the goal in the
 proof script. We do this by “clamping down” selected function symbols
 in the goal, which prevents them from being considered in
 simplification or rewriting steps. This clamping is accomplished by
-using the occurrence switches (see section:ref:`abbreviations_ssr`)
+using the occurrence switches (see section :ref:`abbreviations_ssr`)
 together with “term tagging” operations.
 
 |SSR| provides two levels of tagging.
@@ -4385,7 +4385,7 @@ Contextual patterns in rewrite
 
   Note: the simplification rule ``addSn`` is applied only under the ``f``
   symbol.
-  Then we simplify also the first addition and expand 0 into 0+0.
+  Then we simplify also the first addition and expand ``0`` into ``0 + 0``.
 
   .. coqtop:: all
 
@@ -4738,7 +4738,7 @@ Interpreting assumptions
 Interpreting an assumption in the context of a proof consists in
 applying to it a lemma before generalizing, and/or decomposing this
 assumption. For instance, with the extensive use of boolean reflection
-(see section :ref:`views_and_reflection_ssr`.4), it is quite frequent
+(see section :ref:`views_and_reflection_ssr`), it is quite frequent
 to need to decompose the logical interpretation of (the boolean
 expression of) a fact, rather than the fact itself. This can be
 achieved by a combination of ``move : _ => _`` switches, like in the
@@ -5201,7 +5201,7 @@ There are three steps in the behavior of an assumption view tactic:
 For a ``case/term`` tactic, the generalisation step is replaced by a
 case analysis step.
 
-*View hints* are declared by the user (see section:ref:`views_and_reflection_ssr`.8) and are
+*View hints* are declared by the user (see section :ref:`views_and_reflection_ssr`) and are
 stored in the Hint View database. The proof engine automatically
 detects from the shape of the top assumption ``top`` and of the view lemma
 ``term`` provided to the tactic the appropriate view hint in the