aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Reference-Manual.tex
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@gmail.com>2018-03-22 15:42:38 +0100
committerGravatar GitHub <noreply@github.com>2018-03-22 15:42:38 +0100
commit788e841e51bbe081be522b1ae50e630ea1c3df99 (patch)
tree4b9383a071db90e64abb5d9f1c533d39e159eb57 /doc/refman/Reference-Manual.tex
parentb2ee5fbdcfa5a837a46363b234a1f84799c374e7 (diff)
parenta5aa8da2dcaa62b0abb5e2ce2d466894c5b82b65 (diff)
Merge branch 'master' into sphinx-doc-chapter-22
Diffstat (limited to 'doc/refman/Reference-Manual.tex')
-rw-r--r--doc/refman/Reference-Manual.tex3
1 files changed, 0 insertions, 3 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 4b7f9d91b..86f123322 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -117,11 +117,8 @@ Options A and B of the licence are {\em not} elected.}
%END LATEX
\part{Addendum to the Reference Manual}
\include{AddRefMan-pre}%
-\include{Cases.v}%
\include{Coercion.v}%
-\include{CanonicalStructures.v}%
\include{Classes.v}%
-\include{Omega.v}%
\include{Extraction.v}%
\include{Program.v}%
\include{Polynom.v}% = Ring