Review changes #2

Author: jfehrle

doc/sphinx/language/coq-library.rst

@@ -7,20 +7,19 @@ The |Coq| library
    single: Theories
 
 
-The |Coq| library is structured into two parts:
+The |Coq| library has two parts:
 
-  * **The initial library**: it contains elementary logical notions and
-    data-types. It constitutes the basic state of the system directly
-    available when running |Coq|;
+  * **The basic library**: definitions and theorems for
+    the most commonly used elementary logical notions and
+    data types. |Coq| normally loads these files automatically when it starts.
 
-  * **The standard library**: general-purpose libraries containing various
-    developments of |Coq| axiomatizations about sets, lists, sorting,
-    arithmetic, etc. This library comes with the system and its modules
-    are directly accessible through the ``Require`` command (see
-    Section :ref:`compiled-files`);
+  * **The standard library**: general-purpose libraries with
+    definitions and theorems for sets, lists, sorting,
+    arithmetic, etc. To use these files, users must load them explicitly
+    with the ``Require`` command (see Section :ref:`compiled-files`)
 
-In addition, user-provided libraries or developments are provided by
-|Coq| users' community. These libraries and developments are available
+There are also many libraries provided by |Coq| users' community.
+These libraries and developments are available
 for download at http://coq.inria.fr (see
 Section :ref:`userscontributions`).
 
@@ -514,8 +513,8 @@ realizability interpretation.
    forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P.
 
 
-Basic Arithmetics
-~~~~~~~~~~~~~~~~~
+Basic Arithmetic
+~~~~~~~~~~~~~~~~
 
 The basic library includes a few elementary properties of natural
 numbers, together with the definitions of predecessor, addition and
@@ -804,8 +803,8 @@ Notation          Interpretation
 ===============   ===================
 
 
-Notations for integer arithmetics
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Notations for integer arithmetic
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. index::
   single: Arithmetical notations
@@ -822,7 +821,7 @@ Notations for integer arithmetics
 
 
 The following table describes the syntax of expressions
-for integer arithmetics. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``.
+for integer arithmetic. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``.
 It specifies how notations are interpreted and, when not
 already reserved, the precedence and associativity.
 
@@ -866,7 +865,7 @@ Notations for real numbers
 
 This is provided by requiring and opening the module ``Reals`` and
 opening scope ``R_scope``. This set of notations is very similar to
-the notation for integer arithmetics. The inverse function was added.
+the notation for integer arithmetic. The inverse function was added.
 
 ===============   ===================
 Notation          Interpretation

doc/sphinx/language/gallina-specification-language.rst

@@ -106,20 +106,24 @@ Keywords
 
   Note that plugins may define additional keywords when they are loaded.
 
-Special tokens
-  The set of special
+Other tokens
+  The set of
   tokens defined at any given time can vary because the :cmd:`Notation`
   command can define new tokens.  A :cmd:`Require` command may load more notation definitions,
-  while the end of a :cmd:`Section` may remove notations.
+  while the end of a :cmd:`Section` may remove notations.  Some notations
+  are defined in the basic library (see :ref:`thecoqlibrary`) and are normallly
+  loaded automatically at startup time.
 
-  Here are some of the character sequences that are special tokens::
+
+  Here are the character sequences that Coq directly defines as tokens
+  without using :cmd:`Notation` (omitting 25 specialized tokens that begin with
+  ``#int63_``)::
 
     ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - ->
     . .( .. ... / : ::= := :> :>> ; < <+ <- <:
     <<: <= = => > >-> >= ? @ @{ [ [= ] _ _eqn
     `( `{ { {| | |- || }
 
-
   When multiple tokens match the beginning of a sequence of characters,
   the longest matching token is used.
   Occasionally you may need to insert spaces to separate tokens.  For example,

doc/sphinx/proof-engine/ltac.rst

@@ -34,7 +34,7 @@ in these grammar rules. Various already defined entries will be used in this
 chapter: entries :token:`num`, :token:`int`, :token:`ident`
 :token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic`
 represent respectively natural and integer numbers,
-identifiers, qualified names, terms, patterns and the atomic
+identifiers, qualified names, Coq terms, patterns and the atomic
 tactics described in Chapter :ref:`tactics`.
 
 The syntax of :production:`cpattern` is