aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorMaxime Dénès2018-03-22 11:33:41 +0100
committerMaxime Dénès2018-03-22 11:33:41 +0100
commitbb03fa4eaf74e776b94b7a4b93754742d20f6d3d (patch)
tree47cc558fc1eda5854eef4d17cf93d8559bf3629c /doc
parentef0fc7730df3cb585b621955010115407d80d2e7 (diff)
[Sphinx] Move chapter 22 to new infrastructure
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