aboutsummaryrefslogtreecommitdiff
path: root/doc/refman/Reference-Manual.tex
diff options
context:
space:
mode:
authorThéo Zimmermann2018-04-04 09:47:18 +0200
committerThéo Zimmermann2018-04-04 09:47:18 +0200
commitbec815511e2bff57637bd24fb7accd3238b6db3c (patch)
treedfaa58ba93d0f7c447827b687dd72c7467939c02 /doc/refman/Reference-Manual.tex
parent7e51ffdaf4340a67c254be7800eb8c68c5d78f2c (diff)
parentf84eda17d1e1d15248bab4fb41941b2d6da77ddb (diff)
Merge PR #7047: Sphinx doc chapter 24
Diffstat (limited to 'doc/refman/Reference-Manual.tex')
-rw-r--r--doc/refman/Reference-Manual.tex1
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 3feb9014f5..a652a121c5 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -117,7 +117,6 @@ Options A and B of the licence are {\em not} elected.}
%END LATEX
\part{Addendum to the Reference Manual}
\include{AddRefMan-pre}%
-\include{Program.v}%
\include{Polynom.v}% = Ring
\include{Nsatz.v}%
\include{Setoid.v}% Tactique pour les setoides