Merge PR #8143: Improved grammar and spelling in chapters 'Proof Schemes' and 'The Coq commands' of the Reference Manual.

1 files changed, 14 insertions, 20 deletions

diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 838926d651..ab1edc0b27 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -40,8 +40,7 @@ induction for objects in type `identᵢ`.
 
    Induction scheme for tree and forest.
 
-   The definition of principle of mutual induction for tree and forest
-   over the sort Set is defined by the command:
+   A mutual induction principle for tree and forest in sort ``Set`` can be defined using the command
 
     .. coqtop:: none
 
@@ -193,10 +192,12 @@ command generates the induction principle for each `identᵢ`, following
 the recursive structure and case analyses of the corresponding function 
 identᵢ’.
 
-Remark: There is a difference between obtaining an induction scheme by
-using ``Functional Scheme`` on a function defined by ``Function`` or not.
-Indeed, ``Function`` generally produces smaller principles, closer to the
-definition written by the user.
+.. warning::
+
+   There is a difference between induction schemes generated by the command
+   :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed,
+   :cmd:`Function` generally produces smaller principles that are closer to how
+   a user would implement them. See :ref:`advanced-recursive-functions` for details.
 
 .. example:: 
 
@@ -257,11 +258,6 @@ definition written by the user.
     auto with arith.
     Qed.
 
-  Remark: There is a difference between obtaining an induction scheme
-  for a function by using ``Function`` (see :ref:`advanced-recursive-functions`) and by using
-  ``Functional Scheme`` after a normal definition using ``Fixpoint`` or
-  ``Definition``. See :ref:`advanced-recursive-functions` for details.
-
 .. example::
 
   Induction scheme for tree_size.
@@ -298,15 +294,15 @@ definition written by the user.
     | cons t f' => (tree_size t + forest_size f')
     end.
 
-  Remark: Function generates itself non mutual induction principles
-  tree_size_ind and forest_size_ind:
+  Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind``
+  generated by ``Function`` are not mutual.
 
   .. coqtop:: all
 
     Check tree_size_ind.
 
-  The definition of mutual induction principles following the recursive
-  structure of `tree_size` and `forest_size` is defined by the command:
+  Mutual induction principles following the recursive structure of ``tree_size``
+  and ``forest_size`` can be generated by the following command:
 
   .. coqtop:: all
 
@@ -352,10 +348,8 @@ having inverted the instance with the tactic `inversion`.
 
 .. example::
 
-  Let us consider the relation `Le` over natural numbers and the following
-  variable:
-
-  .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning
+  Consider the relation `Le` over natural numbers and the following
+  parameter ``P``:
   
   .. coqtop:: all
 
@@ -363,7 +357,7 @@ having inverted the instance with the tactic `inversion`.
     | LeO : forall n:nat, Le 0 n
     | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
 
-    Axiom P : nat -> nat -> Prop.
+    Parameter P : nat -> nat -> Prop.
 
   To generate the inversion lemma for the instance `(Le (S n) m)` and the
   sort `Prop`, we do: