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

12 files changed, 6 insertions, 34 deletions

diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index 2cc1f95c08..3e414a714c 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -1,4 +1,3 @@
-.. include:: ../replaces.rst
 .. _canonicalstructures:
 
 Canonical Structures
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index e507a224c6..ad6a06d2b0 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _extendedpatternmatching:
 
 Extended pattern-matching
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index e3d25cf5cf..4bfa45d54c 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _extraction:
 
 Extraction of programs in |OCaml| and Haskell
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index e0babb6c4e..403b163196 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
 .. _generalizedrewriting:
 
 Generalized rewriting
@@ -126,10 +123,10 @@ parameters is any term :math:`f \, t_1 \ldots t_n`.
 
    .. coqtop:: in
 
-     forall (A : Type) (S1 S1’ S2 S2’ : list A),
-       set_eq A S1 S1’ ->
-       set_eq A S2 S2’ ->
-       set_eq A (union A S1 S2) (union A S1’ S2’).
+     forall (A: Type) (S1 S1' S2 S2': list A),
+       set_eq A S1 S1' ->
+       set_eq A S2 S2' ->
+       set_eq A (union A S1 S2) (union A S1' S2').
 
    The signature of the function ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A``
    for all ``A``.
@@ -451,7 +448,7 @@ various combinations of properties on relations and morphisms are
 represented as records and instances of theses classes are put in a
 hint database. For example, the declaration:
 
-.. coqtop:: in
+.. coqdoc::
 
    Add Parametric Relation (x1 : T1) ... (xn : Tn) : (A t1 ... tn) (Aeq t′1 ... t′m)
      [reflexivity proved by refl]
@@ -462,7 +459,7 @@ hint database. For example, the declaration:
 
 is equivalent to an instance declaration:
 
-.. coqtop:: in
+.. coqdoc::
 
    Instance (x1 : T1) ... (xn : Tn) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) :=
      [Equivalence_Reflexive := refl]
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 23cbd76eda..5cb0eaf469 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _implicitcoercions:
 
 Implicit Coercions
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index 0f2d35d044..2cde65dcdc 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _miscellaneousextensions:
 
 Miscellaneous extensions
diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst
index 9adeca46fc..e7a8c238ac 100644
--- a/doc/sphinx/addendum/nsatz.rst
+++ b/doc/sphinx/addendum/nsatz.rst
@@ -1,5 +1,3 @@
-.. include:: ../preamble.rst
-
 .. _nsatz_chapter:
 
 Nsatz: tactics for proving equalities in integral domains
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index 8ee8f52227..eb19d57203 100644
--- a/doc/sphinx/addendum/parallel-proof-processing.rst
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _asynchronousandparallelproofprocessing:
 
 Asynchronous and Parallel Proof Processing
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index d6895f5fe5..24247f7bb1 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -1,6 +1,3 @@
-.. include:: ../preamble.rst
-.. include:: ../replaces.rst
-
 .. this should be just "_program", but refs to it don't work
 
 .. _programs:
@@ -378,6 +375,3 @@ Frequently Asked Questions
        using lazy evaluation;
     #. Mutual recursion on the underlying inductive type isn’t possible
        anymore, but nested mutual recursion is always possible.
-
-.. bibliography:: ../biblio.bib
-   :keyprefix: p-
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 8cb86e2267..58617916c0 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -1,11 +1,9 @@
-.. include:: ../replaces.rst
 .. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}`
 .. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}`
 .. |eq| replace:: `=`:sub:`(by the main correctness theorem)`
 .. |re| replace:: ``(PEeval`` `v` `ap`\ ``)``
 .. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))``
 
-
 .. _theringandfieldtacticfamilies:
 
 The ring and field tactic families
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index ab4b4a9824..418014809f 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _typeclasses:
 
 Type Classes
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 7e77dea457..706ce1065c 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -1,5 +1,3 @@
-.. include:: ../replaces.rst
-
 .. _polymorphicuniverses:
 
 Polymorphic Universes