Apply suggestions from code review

Co-Authored-By: gares <gares@fettunta.org>

1 files changed, 4 insertions, 4 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index d40474188f..ae721c2430 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1598,12 +1598,12 @@ Views
 The first entry in the :token:`i_view` grammar rule, :n:`/@term`,
 represents a view (see section :ref:`views_and_reflection_ssr`).
 It interprets the top of the stack with the view :token:`term`.
-It is equivalent to ``move/term``.
+It is equivalent to :n:`move/@term`.
 
 A :token:`clear_switch` that immediately precedes an :token:`i_view`
 that happen to be a :token:`ident` is extended with that
 :token:`ident` and the :token:`clear_switch` is executed after the view.
-Eg ``{}/v`` is equivalent to ``/v{v}``.
+E.g. ``{}/v`` is equivalent to ``/v{v}``.
 
 If the next :token:`i_item` is a view, then the view is
 applied to the assumption in top position once all the
@@ -1628,7 +1628,7 @@ Intro patterns
   a new constant, fact, or defined constant :token:`ident`, respectively.
   Note that defined constants cannot be introduced when δ-expansion is
   required to expose the top variable or assumption.
-  A :token:`clear_switch` (even an empty one) immediately preceding a
+  A :token:`clear_switch` (even an empty one) immediately preceding an
   :token:`ident` is extended with that :token:`ident` if the identifier
   points to an existing context entry. As a consequence  by prefixing the
   :token:`ident` with ``{}`` one can *replace* a context entry.
@@ -3065,7 +3065,7 @@ operation should be performed:
   the occurrences of the rewrite pattern which should be affected by the
   rewrite operation.
 
-  A clear switch, even an empty one, is is performed *after* the
+  A clear switch, even an empty one, is performed *after* the
   :token:`r_item` is actually processed and is complemented with the name of
   the rewrite rule when it is a simple context entry. As a consequence one can
   write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately