Merge PR #8070: Fixed some typos and grammar errors from section 'The language' of the Reference Manual.

3 files changed, 23 insertions, 15 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index b01a4ef0f..98e81ebc6 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1175,7 +1175,7 @@ ourselves to primitive recursive functions and functionals.
 
 For instance, assuming a parameter :g:`A:Set` exists in the local context,
 we want to build a function length of type :g:`list A -> nat` which computes
-the length of the list, so such that :g:`(length (nil A)) = O` and :g:`(length
+the length of the list, such that :g:`(length (nil A)) = O` and :g:`(length
 (cons A a l)) = (S (length l))`. We want these equalities to be
 recognized implicitly and taken into account in the conversion rule.
 
@@ -1364,7 +1364,7 @@ irrelevance property which is sometimes a useful axiom:
 The elimination of an inductive definition of type :math:`\Prop` on a predicate
 :math:`P` of type :math:`I→ Type` leads to a paradox when applied to impredicative
 inductive definition like the second-order existential quantifier
-:g:`exProp` defined above, because it give access to the two projections on
+:g:`exProp` defined above, because it gives access to the two projections on
 this type.
 
 
@@ -1613,7 +1613,7 @@ then the recursive
 arguments will correspond to :math:`T_i` in which one of the :math:`I_l` occurs.
 
 The main rules for being structurally smaller are the following.
-Given a variable :math:`y` of type an inductive definition in a declaration
+Given a variable :math:`y` of an inductively defined type in a declaration
 :math:`\ind{r}{Γ_I}{Γ_C}` where :math:`Γ_I` is :math:`[I_1 :A_1 ;…;I_k :A_k]`, and :math:`Γ_C` is
 :math:`[c_1 :C_1 ;…;c_n :C_n ]`, the terms structurally smaller than :math:`y` are:
 
@@ -1625,7 +1625,7 @@ Given a variable :math:`y` of type an inductive definition in a declaration
   Each :math:`f_i` corresponds to a type of constructor
   :math:`C_q ≡ ∀ p_1 :P_1 ,…,∀ p_r :P_r , ∀ y_1 :B_1 , … ∀ y_k :B_k , (I~a_1 … a_k )`
   and can consequently be written :math:`λ y_1 :B_1' . … λ y_k :B_k'. g_i`. (:math:`B_i'` is
-  obtained from :math:`B_i` by substituting parameters variables) the variables
+  obtained from :math:`B_i` by substituting parameters for variables) the variables
   :math:`y_j` occurring in :math:`g_i` corresponding to recursive arguments :math:`B_i` (the
   ones in which one of the :math:`I_l` occurs) are structurally smaller than y.
 
@@ -1801,7 +1801,7 @@ definitions can be found in :cite:`Gimenez95b,Gim98,GimCas05`.
 
 .. _The-Calculus-of-Inductive-Construction-with-impredicative-Set:
 
-The Calculus of Inductive Construction with impredicative Set
+The Calculus of Inductive Constructions with impredicative Set
 -----------------------------------------------------------------
 
 |Coq| can be used as a type-checker for the Calculus of Inductive
@@ -1834,7 +1834,7 @@ inductive definitions* like the example of second-order existential
 quantifier (:g:`exSet`).
 
 There should be restrictions on the eliminations which can be
-performed on such definitions. The eliminations rules in the
+performed on such definitions. The elimination rules in the
 impredicative system for sort :math:`\Set` become:
 
 
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index f23e04c3a..52c56d2bd 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -705,21 +705,29 @@ fixpoint equation can be proved.
 Accessing the Type level
 ~~~~~~~~~~~~~~~~~~~~~~~~
 
-The basic library includes the definitions of the counterparts of some data-types and logical
-quantifiers at the ``Type``: level: negation, pair, and properties
-of ``identity``. This is the module ``Logic_Type.v``.
+The standard library includes ``Type`` level definitions of counterparts of some
+logic concepts and basic lemmas about them.
+
+The module ``Datatypes`` defines ``identity``, which is the ``Type`` level counterpart
+of equality:
+
+.. index::
+   single: identity (term)
+
+.. coqtop:: in
+
+   Inductive identity (A:Type) (a:A) : A -> Type :=
+     identity_refl : identity a a.
+
+Some properties of ``identity`` are proved in the module ``Logic_Type``, which also
+provides the definition of ``Type`` level negation:
 
 .. index::
   single: notT (term)
-  single: prodT (term)
-  single: pairT (term)
 
 .. coqtop:: in
 
   Definition notT (A:Type) := A -> False.
-  Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B).
-
-At the end, it defines data-types at the ``Type`` level.
 
 Tactics
 ~~~~~~~
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 509ac92f8..d9b249045 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1079,7 +1079,7 @@ The definition of ``N`` using the module type expression ``SIG`` with
 
    Module N : SIG' := M.
 
-If we just want to be sure that the our implementation satisfies a
+If we just want to be sure that our implementation satisfies a
 given module type without restricting the interface, we can use a
 transparent constraint