Apply suggestions from code review

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

2 files changed, 6 insertions, 6 deletions

diff --git a/CHANGES.md b/CHANGES.md
index b2f9f7926d..3ef0043672 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -163,12 +163,12 @@ SSReflect
   - replace hypothesis: => {}H
   See the reference manual for the actual documentation.
 
-- Clear discipline made consistent across the entire proof language language.
+- Clear discipline made consistent across the entire proof language.
   Whenever a clear switch {x..} comes immediately before an existing proof
   context entry (used as a view, as a rewrite rule or as name for a new
   context entry) then such entry is cleared too.
 
-  Eg. The following sentences are elaborated as follows (when H is an existing
+  E.g. The following sentences are elaborated as follows (when H is an existing
   proof context entry):
   - "=> {x..} H"       ->  "=> {x..H} H"
   - "=> {x..} /H"      ->  "=> /v {x..H}"
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