aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-29 17:18:52 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-04 14:05:57 +0200
commitdd10128c6cd822c1a16109bffc5b4fb67dc3ce49 (patch)
treef70eac5c4b4ae9bf7222d9ed308eb3d919abe012 /doc
parentb301358a7cbe3f53cc3d0e9b35f930ccd23adae2 (diff)
[Sphinx] Move chapter 28 to new infrastructure
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/Reference-Manual.tex1
-rw-r--r--doc/sphinx/addendum/parallel-proof-processing.rst (renamed from doc/refman/AsyncProofs.tex)0
2 files changed, 0 insertions, 1 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index cfb3c625b..7e68dd752 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{AsyncProofs}% Paral-ITP
\include{Universes.v}% Universe polymorphes
\include{Misc.v}
%BEGIN LATEX
diff --git a/doc/refman/AsyncProofs.tex b/doc/sphinx/addendum/parallel-proof-processing.rst
index 8f9d876cb..8f9d876cb 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst