Merge PR #8418: Add a PDF version of the manual

4 files changed, 25 insertions, 27 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index ac0f0f8ea6..c8c3e37efb 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
 .. _calculusofinductiveconstructions:
 
 
@@ -1010,7 +1007,7 @@ the Type hierarchy.
 
    It is possible to declare the same inductive definition in the
    universe :math:`\Type`. The :g:`exType` inductive definition has type
-   :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}`
+   :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT}_{\kw{intro}}`
    has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`.
 
    .. coqtop:: all
@@ -1264,14 +1261,14 @@ The |Coq| term for this proof
 will be written:
 
 .. math::
-   \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \endkw
+   \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \kwend
 
 In this expression, if :math:`m` eventually happens to evaluate to
 :math:`(c_i~u_1 … u_{p_i})` then the expression will behave as specified in its :math:`i`-th branch
 and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are replaced by the
 :math:`u_1 … u_{p_i}` according to the ι-reduction.
 
-Actually, for type checking a :math:`\Match…\with…\endkw` expression we also need
+Actually, for type checking a :math:`\Match…\with…\kwend` expression we also need
 to know the predicate P to be proved by case analysis. In the general
 case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate
 over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I`
@@ -1285,7 +1282,7 @@ using the syntax:
 .. math::
    \Match~m~\as~x~\In~I~\_~a~\return~P~\with~
    (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | …
-   | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\endkw
+   | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend
    
 The :math:`\as` part can be omitted if either the result type does not depend
 on :math:`m` (non-dependent elimination) or :math:`m` is a variable (in this case, :math:`m`
@@ -1471,6 +1468,8 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:
    where
 
    .. math::
+      :nowrap:
+
       \begin{eqnarray*}
         P & = & \lambda~l~.~P^\prime\\
         f_1 & = & t_1\\
@@ -1711,13 +1710,15 @@ for primitive recursive operators. The following reductions are now
 possible:
 
 .. math::
-   \def\plus{\mathsf{plus}}
-   \def\tri{\triangleright_\iota}
-   \begin{eqnarray*}
-   \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
-                                  & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
-                                  & \tri & \nS~(\nS~(\nS~\nO))\\
-   \end{eqnarray*}
+   :nowrap:
+
+   {\def\plus{\mathsf{plus}}
+    \def\tri{\triangleright_\iota}
+    \begin{eqnarray*}
+    \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
+                                   & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
+                                   & \tri & \nS~(\nS~(\nS~\nO))\\
+    \end{eqnarray*}}
 
 .. _Mutual-induction:
 
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 9de30e2190..320448d46e 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _thecoqlibrary:
 
 The |Coq| library
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 0fbe7ac70b..27ed176a9b 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _extensionsofgallina:
 
 Extensions of |Gallina|
@@ -22,7 +20,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
 
 .. _record_grammar:
 
-  .. productionlist:: `sentence`
+  .. productionlist:: sentence
      record         : `record_keyword` `record_body` with … with `record_body`
      record_keyword : Record | Inductive | CoInductive
      record_body    : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }.
@@ -82,11 +80,13 @@ To build an object of type :n:`@ident`, one should provide the constructor
        Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
        Check half.
 
+.. FIXME: move this to the main grammar in the spec chapter
+
 .. _record-named-fields-grammar:
 
   .. productionlist::
-    term : {| [`field_def` ; … ; `field_def`] |}
-    field_def : name [binders] := `term`
+    record_term : {| [`field_def` ; … ; `field_def`] |}
+    field_def : name [binders] := `record_term`
 
 Alternatively, the following syntax allows creating objects by using named fields, as
 shown in this grammar. The fields do not have to be in any particular order, nor do they have
@@ -154,12 +154,14 @@ It can be activated for printing with
        Set Printing Projections.
        Check top half.
 
+.. FIXME: move this to the main grammar in the spec chapter
+
 .. _record_projections_grammar:
 
   .. productionlist:: terms
-     term : term `.` ( qualid )
-          : | term `.` ( qualid arg … arg )
-          : | term `.` ( @`qualid` `term` … `term` )
+     projection : projection `.` ( `qualid` )
+          : | projection `.` ( `qualid` `arg` … `arg` )
+          : | projection `.` ( @`qualid` `term` … `term` )
 
   Syntax of Record projections
 
diff --git a/doc/sphinx/language/module-system.rst b/doc/sphinx/language/module-system.rst
index e6a6736654..15fee91245 100644
--- a/doc/sphinx/language/module-system.rst
+++ b/doc/sphinx/language/module-system.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
 .. _themodulesystem:
 
 The Module System