aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Reference-Manual.tex
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-13 10:32:47 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-13 10:32:47 +0200
commitb68e0b4f9ba37d1c2fa5921e1d934b4b38bfdfe7 (patch)
treea6fcfbb975fe7dd1c4b29bebdbfacb4e300f4807 /doc/refman/Reference-Manual.tex
parent43053e7e025e57f00741bcd744c20bc6f2c583af (diff)
parent92c604f8b331c3e202d8477019e183c2cfef9f41 (diff)
Merge PR #7117: Sphinx doc chapter 29
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 061686e12..d373f76bf 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -109,7 +109,6 @@ Options A and B of the licence are {\em not} elected.}
%END LATEX
\part{Addendum to the Reference Manual}
\include{AddRefMan-pre}%
-\include{Universes.v}% Universe polymorphes
%BEGIN LATEX
\RefManCutCommand{ENDADDENDUM=\thepage}
%END LATEX