aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-22 10:01:01 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-22 10:01:01 +0100
commitdb6262fd028086c6201fe4894243fcf691c65099 (patch)
tree2bd297e427890d3e8b65b1d62369c2c53cb8c6c3 /doc
parentef0fc7730df3cb585b621955010115407d80d2e7 (diff)
[Sphinx] Move chapter 17 to new infrastructure
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/Reference-Manual.tex1
-rw-r--r--doc/sphinx/addendum/extended-pattern-matching.rst (renamed from doc/refman/Cases.tex)0
2 files changed, 0 insertions, 1 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 231742e56..7ef676ba9 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{Cases.v}%
\include{Coercion.v}%
\include{CanonicalStructures.v}%
\include{Classes.v}%
diff --git a/doc/refman/Cases.tex b/doc/sphinx/addendum/extended-pattern-matching.rst
index 376ef031d..376ef031d 100644
--- a/doc/refman/Cases.tex
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst