aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Reference-Manual.tex
diff options
context:
space:
mode:
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