aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorMaxime Dénès2018-03-22 14:49:42 +0100
committerMaxime Dénès2018-03-29 14:00:08 +0200
commit98fc90ba52d0c2e2837001538117562ce9caefd6 (patch)
treeb613d66a271e708fce619438fb5f124e88f877cb /doc
parent1fa0a403cd167796fd082be87828cec610a209ca (diff)
[Sphinx] Move chapter 24 to new infrastructure
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/Reference-Manual.tex1
-rw-r--r--doc/sphinx/addendum/program.rst (renamed from doc/refman/Program.tex)0
2 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
diff --git a/doc/refman/Program.tex b/doc/sphinx/addendum/program.rst
index 1e204dc83d..1e204dc83d 100644
--- a/doc/refman/Program.tex
+++ b/doc/sphinx/addendum/program.rst