diff options
| author | Guillaume Melquiond | 2018-03-22 15:39:11 +0100 |
|---|---|---|
| committer | GitHub | 2018-03-22 15:39:11 +0100 |
| commit | 6c1ccc200cff1ade5e07d60d6458b4471cde551d (patch) | |
| tree | 22f72b0ce66329ffe496b8162d4bcc942d9365fd /doc/refman/Reference-Manual.tex | |
| parent | 109106cbd36d169de839066da4f3265f291bc924 (diff) | |
| parent | 31a8690728ea2308e5adc1c429981c4779093615 (diff) | |
Merge branch 'master' into sphinx-doc-chapter-21
Diffstat (limited to 'doc/refman/Reference-Manual.tex')
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index afc1b9c57f..a49637bb2a 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -117,9 +117,7 @@ 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}% \include{Micromega.v} \include{Extraction.v}% |