aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/Reference-Manual.tex1
-rw-r--r--doc/sphinx/addendum/micromega.rst (renamed from doc/refman/Micromega.tex)0
2 files changed, 0 insertions, 1 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 231742e569..4b7f9d91b2 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -122,7 +122,6 @@ Options A and B of the licence are {\em not} elected.}
\include{CanonicalStructures.v}%
\include{Classes.v}%
\include{Omega.v}%
-\include{Micromega.v}
\include{Extraction.v}%
\include{Program.v}%
\include{Polynom.v}% = Ring
diff --git a/doc/refman/Micromega.tex b/doc/sphinx/addendum/micromega.rst
index 2617142f5a..2617142f5a 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/sphinx/addendum/micromega.rst