Integration of a sphinx-based documentation generator.

The original contribution is from Clément Pit-Claudel. I updated
his code and integrated it with the Coq build system. Many improvements
by Paul Steckler (MIT).

This commit adds the infrastructure but no content.

12 files changed, 1632 insertions, 0 deletions

diff --git a/doc/sphinx/MIGRATING b/doc/sphinx/MIGRATING
new file mode 100644
index 0000000000..fa6fe15379
--- /dev/null
+++ b/doc/sphinx/MIGRATING
@@ -0,0 +1,238 @@
+How to migrate the Coq Reference Manual to Sphinx
+=================================================
+
+# Install Python3 packages (requires Python 3, python3-pip, python3-setuptools)
+
+  * pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex
+
+# You may want to do this under a virtualenv, particularly if you end up with issues finding sphinxcontrib.bibtex. http://docs.python-guide.org/en/latest/dev/virtualenvs/
+
+  * pip3 install virtualenv
+  * virtualenv coqsphinxing # you may want to use -p to specify the python version
+  * source coqsphinxing/bin/activate # activate the virtual environment
+
+# After activating the virtual environment you can run the above pip3 command to install sphinx. You will have to activate the virtual environment before building the docs in your session.
+
+# Add this Elisp code to .emacs, if you're using emacs (recommended):
+
+ (defun sphinx/quote-coq-refman-region (left right &optional beg end count)
+   (unless beg
+     (if (region-active-p)
+         (setq beg (region-beginning) end (region-end))
+       (setq beg (point) end nil)))
+   (unless count
+     (setq count 1))
+   (save-excursion
+     (goto-char (or end beg))
+     (dotimes (_ count) (insert right)))
+   (save-excursion
+     (goto-char beg)
+     (dotimes (_ count) (insert left)))
+   (if (and end (characterp left)) ;; Second test handles the ::`` case
+       (goto-char (+ (* 2 count) end))
+     (goto-char (+ count beg))))
+
+ (defun sphinx/coqtop (beg end)
+   (interactive (list (region-beginning) (region-end)))
+   (replace-regexp "^Coq < " "      " nil beg end)
+   (indent-rigidly beg end -3)
+   (goto-char beg)
+   (insert ".. coqtop:: all\n\n"))
+
+ (defun sphinx/rst-coq-action ()
+   (interactive)
+   (pcase (read-char "Command?")
+     (?g (sphinx/quote-coq-refman-region ":g:`" "`"))
+     (?n (sphinx/quote-coq-refman-region ":n:`" "`"))
+     (?t (sphinx/quote-coq-refman-region ":token:`" "`"))
+     (?m (sphinx/quote-coq-refman-region ":math:`" "`"))
+     (?: (sphinx/quote-coq-refman-region "::`" "`"))
+     (?` (sphinx/quote-coq-refman-region "``" "``"))
+     (?c (sphinx/coqtop (region-beginning) (region-end)))))
+
+ (global-set-key (kbd "<f12>") #'sphinx/rst-coq-action)
+
+ With this code installed, you can hit "F12" followed by an appropriate key to do quick markup of text
+ (this will make more sense once you've started editing the text).
+
+# Fork the Coq repo, if needed:
+
+ https://github.com/coq/coq
+
+# Clone the repo to your work machine
+
+# Add Maxime Dénès's repo as a remote:
+
+ git remote add sphinx https://github.com/maximedenes/coq.git
+
+  (or choose a name other than "sphinx")
+
+ Verify with:
+
+ git remote -v
+
+# Fetch from the remote
+
+ git fetch sphinx
+
+# Checkout the sphinx-doc branch
+
+   git checkout sphinx-doc
+
+  You should pull from the repo from time to time to keep your local copy up-to-date:
+
+   git pull sphinx sphinx-doc
+
+  You may want to create a new branch to do your work in.
+
+# Choose a Reference Manual chapter to work on at
+
+    https://docs.google.com/document/d/1Yo7dV4OI0AY9Di-lsEQ3UTmn5ygGLlhxjym7cTCMCWU
+
+# For each chapter, raw ReStructuredText (the Sphinx format), created by the "html2rest" utility,
+   is available in the directory porting/raw-rst/
+
+  Elsewhere, depending on the chapter, there should be an almost-empty template file already created,
+   which is in the location where the final version should go
+
+# Manually edit the .rst file, place it in the correct location
+
+  There are small examples in sphinx/porting/, a larger example in language/gallina-extensions.rst
+
+  (N.B.: the migration is a work-in-progress, your suggestions are welcome)
+
+  Find the chapter you're working on from the online manual at https://coq.inria.fr/distrib/current/refman/.
+  At the top of the file, after the chapter heading, add:
+
+    :Source: https://coq.inria.fr/distrib/current/refman/the-chapter-file.html
+    :Converted by: Your Name
+
+  N.B.: These source and converted-by annotations should help for the migration phase. Later on,
+  those annotations will be removed, and contributors will be mentioned in the Coq credits.
+
+  Remove chapter numbers
+
+  Replace section, subsection numbers with reference labels:
+
+    .. _some-reference-label:
+
+  Place the label before the section or subsection, followed by a blank line.
+
+  Note the leading underscore. Use :ref:`some_reference-label` to refer to such a label; note the leading underscore is omitted.
+  Many cross-references may be to other chapters. If the required label exists, use it. Otherwise, use a dummy reference of the form
+  `TODO-n.n.n-mnemonic` we can fixup later. Example:
+
+    :ref:`TODO-1.3.2-definitions`
+
+  We can grep for those TODOs, and the existing subsection number makes it easy to find in the exisyting manual.
+
+  For the particular case of references to chapters, we can use a
+convention for the cross-reference name, so no TODO is needed.
+
+    :ref:`thegallinaspecificationlanguage`
+
+That is, the chapter label is the chapter title, all in lower-case,
+with no spaces or punctuation. For chapters with subtitles marked with
+a ":", like those for Omega and Nsatz, use just the chapter part
+preceding the ":". These labels should already be in the
+placeholder .rst files for each chapter.
+
+
+  You can also label other items, like grammars, with the same syntax. To refer to such labels, not involving a
+  section or subsection, use the syntax
+
+    :ref:`Some link text <label-name>`
+
+  Yes, the angle-brackets are needed here!
+
+  For bibliographic references (those in biblio.bib), use :cite:`thecitation`.
+
+  Grammars will get mangled by the translation. Look for "productionlist" in the examples, also see
+  http://www.sphinx-doc.org/en/stable/markup/para.html.
+
+  For Coq examples that appear, look at the "coqtop" syntax in porting/tricky-bits.rst. The Sphinx
+  script will run coqtop on those examples, and can show the output (or not).
+
+  The file replaces.rst contains replacement definitions for some items that are clumsy to write out otherwise.
+  Use
+
+    .. include:: replaces.rst
+
+  to gain access to those definitions in your file (you might need a path prefix). Some especially-important
+  replacements are |Cic|, |Coq|, |CoqIDE|, and |Gallina|, which display those names in small-caps. Please use them,
+  so that they're rendered consistently.
+
+  Similarly, there are some LaTeX macros in preamble.rst that can be useful.
+
+  Conventions:
+
+    - Keywords and other literal text is double-backquoted (e.g. ``Module``, ``Section``, ``(``, ``,``).
+
+    - Metavariables are single-backquotes (e.g. `term`, `ident`)
+
+    - Use the cmd directive for Vernacular commands, like:
+
+      .. cmd:: Set Printing All.
+
+      Within this directive, prefix metavariables (ident, term) with @:
+
+      .. cmd:: Add Printing Let @ident.
+
+      There's also the "cmdv" directive for variants of a command.
+
+    - Use the "exn" and "warn" directives for errors and warnings:
+
+      .. exn:: Something's not right.
+      .. warn:: You shouldn't do that.
+
+    - Use the "example" directive for examples
+
+    - Use the "g" role for inline Gallina, like :g:`fun x => x`
+
+    - Use code blocks for blocks of Gallina. You can use a double-colon at the end of a line::
+
+        your code here
+
+      which prints a single colon, or put the double-colon on a newline.
+
+::
+
+        your other code here
+
+# Making changes to the text
+
+  The goal of the migration is simply to change the storage format from LaTeX to ReStructuredText. The goal is not
+  to make any organizational or other substantive changes to the text. If you do notice nits (misspellings, wrong
+  verb tense, and so on), please do change them. For example, the programming language that Coq is written in is these days
+  called "OCaml", and there are mentions of the older name "Objective Caml" in the reference manual that should be changed.
+
+# Build, view the manual
+
+  In the root directory of your local repo, run "make sphinx". You can view the result in a browser by loading the HTML file
+  associated with your chapter, which will be contained in the directory doc/sphinx/_build/html/ beneath the repo root directory.
+  Make any changes you need until there are no build warnings and the output is perfect. :-)
+
+# Creating pull requests
+
+  When your changes are done, commit them, push to your fork:
+
+   git commit -m "useful commit message" file
+   git push origin sphinx-doc
+
+  (or push to another branch, if you've created one). Then go to your GitHub
+  fork and create a pull request against Maxime's sphinx-doc
+  branch. If your commit is recent, you should see a link on your
+  fork's code page to do that. Otherwise, you may need to go to your
+  branch on GitHub to do that.
+
+# Issues/Questions/Suggestions
+
+  As the migration proceeds, if you have technical issues, have a more general question, or want to suggest something, please contact:
+
+    Paul Steckler <steck@stecksoft.com>
+    Maxime Dénès <maxime.denes@inria.fr>
+
+# Issues
+
+  Should the stuff in replaces.rst go in preamble.rst?
+  In LaTeX, some of the grammars add productions to existing nonterminals, like term ++= ... . How to indicate that?
diff --git a/doc/sphinx/_static/UbuntuMono-Square.ttf b/doc/sphinx/_static/UbuntuMono-Square.ttf
new file mode 100644
index 0000000000..12b7c6d51a
--- /dev/null
+++ b/doc/sphinx/_static/UbuntuMono-Square.ttf
diff --git a/doc/sphinx/_static/ansi-dark.css b/doc/sphinx/_static/ansi-dark.css
new file mode 100644
index 0000000000..a564fd70bb
--- /dev/null
+++ b/doc/sphinx/_static/ansi-dark.css
@@ -0,0 +1,144 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+.ansi-bold {
+    font-weight: bold;
+}
+
+.ansi-italic {
+    font-style: italic;
+}
+
+.ansi-negative {
+    filter: invert(100%);
+}
+
+.ansi-underline {
+    text-decoration: underline;
+}
+
+.ansi-no-bold {
+    font-weight: normal;
+}
+
+.ansi-no-italic {
+    font-style: normal;
+}
+
+.ansi-no-negative {
+    filter: invert(0%);
+}
+
+.ansi-no-underline {
+    text-decoration: none;
+}
+
+.ansi-black {
+    color: #000000;
+}
+
+.ansi-fg-red {
+    color: #b21717;
+}
+
+.ansi-fg-green {
+    color: #17b217;
+}
+
+.ansi-fg-yellow {
+    color: #b26717;
+}
+
+.ansi-fg-blue {
+    color: #1717b2;
+}
+
+.ansi-fg-magenta {
+    color: #b217b2;
+}
+
+.ansi-fg-cyan {
+    color: #17b2b2;
+}
+
+.ansi-fg-white {
+    color: #b2b2b2;
+}
+
+.ansi-fg-default {
+    color: #404040;
+}
+
+.ansi-fg-light-black {
+    color: #686868;
+}
+
+.ansi-fg-light-red {
+    color: #ff5454;
+}
+
+.ansi-fg-light-green {
+    color: #54ff54;
+}
+
+.ansi-fg-light-yellow {
+    color: #ffff54;
+}
+
+.ansi-fg-light-blue {
+    color: #5454ff;
+}
+
+.ansi-fg-light-magenta {
+    color: #ff54ff;
+}
+
+.ansi-fg-light-cyan {
+    color: #54ffff;
+}
+
+.ansi-fg-light-white {
+    color: #ffffff;
+}
+
+.ansi-bg-black {
+    background-color: #000000;
+}
+
+.ansi-bg-red {
+    background-color: #b21717;
+}
+
+.ansi-bg-green {
+    background-color: #17b217;
+}
+
+.ansi-bg-yellow {
+    background-color: #b26717;
+}
+
+.ansi-bg-blue {
+    background-color: #1717b2;
+}
+
+.ansi-bg-magenta {
+    background-color: #b217b2;
+}
+
+.ansi-bg-cyan {
+    background-color: #17b2b2;
+}
+
+.ansi-bg-white {
+    background-color: #b2b2b2;
+}
+
+.ansi-bg-default {
+    background-color: transparent;
+}
diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css
new file mode 100644
index 0000000000..26bd797709
--- /dev/null
+++ b/doc/sphinx/_static/ansi.css
@@ -0,0 +1,145 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+.ansi-bold {
+    font-weight: bold;
+}
+
+.ansi-italic {
+    font-style: italic;
+}
+
+.ansi-negative {
+    filter: invert(100%);
+}
+
+.ansi-underline {
+    text-decoration: underline;
+}
+
+.ansi-no-bold {
+    font-weight: normal;
+}
+
+.ansi-no-italic {
+    font-style: normal;
+}
+
+.ansi-no-negative {
+    filter: invert(0%);
+}
+
+.ansi-no-underline {
+    text-decoration: none;
+}
+
+
+.ansi-fg-black {
+    color: #babdb6;
+}
+
+.ansi-fg-red {
+    color: #a40000;
+}
+
+.ansi-fg-green {
+    color: #4e9a06;
+}
+
+.ansi-fg-yellow {
+    color: #ce5c00;
+}
+
+.ansi-fg-blue {
+    color: #204a87;
+}
+
+.ansi-fg-magenta {
+    color: #5c3566;
+}
+
+.ansi-fg-cyan {
+    color: #8f5902;
+}
+
+.ansi-fg-white {
+    color: #2e3436;
+}
+
+.ansi-fg-light-black {
+    color: #d3d7cf;
+}
+
+.ansi-fg-light-red {
+    color: #cc0000;
+}
+
+.ansi-fg-light-green {
+    color: #346604;             /* From tango.el */
+}
+
+.ansi-fg-light-yellow {
+    color: #f57900;
+}
+
+.ansi-fg-light-blue {
+    color: #3465a4;
+}
+
+.ansi-fg-light-magenta {
+    color: #75507b;
+}
+
+.ansi-fg-light-cyan {
+    color: #c14d11;
+}
+
+.ansi-fg-light-white {
+    color: #555753;
+}
+
+.ansi-fg-default {
+    color: #eeeeec;
+}
+
+.ansi-bg-black {
+    background-color: #babdb6;
+}
+
+.ansi-bg-red {
+    background-color: #a40000;
+}
+
+.ansi-bg-green {
+    background-color: #4e9a06;
+}
+
+.ansi-bg-yellow {
+    background-color: #ce5c00;
+}
+
+.ansi-bg-blue {
+    background-color: #204a87;
+}
+
+.ansi-bg-magenta {
+    background-color: #5c3566;
+}
+
+.ansi-bg-cyan {
+    background-color: #8f5902;
+}
+
+.ansi-bg-white {
+    background-color: #2e3436;
+}
+
+.ansi-bg-default {
+    background-color: transparent;
+}
diff --git a/doc/sphinx/_static/coqdoc.css b/doc/sphinx/_static/coqdoc.css
new file mode 100644
index 0000000000..bbcc044a20
--- /dev/null
+++ b/doc/sphinx/_static/coqdoc.css
@@ -0,0 +1,68 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+/* Taken from CoqDoc's default stylesheet */
+
+.coqdoc-constructor {
+    color: rgb(60%,0%,0%);
+}
+
+.coqdoc-var {
+    color: rgb(40%,0%,40%);
+}
+
+.coqdoc-variable {
+    color: rgb(40%,0%,40%);
+}
+
+.coqdoc-definition {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-abbreviation {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-lemma {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-instance {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-projection {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-method {
+    color: rgb(0%,40%,0%);
+}
+
+.coqdoc-inductive {
+    color: rgb(0%,0%,80%);
+}
+
+.coqdoc-record {
+    color: rgb(0%,0%,80%);
+}
+
+.coqdoc-class {
+    color: rgb(0%,0%,80%);
+}
+
+.coqdoc-keyword {
+    color : #cf1d1d;
+}
+
+/* Custom additions */
+
+.coqdoc-tactic {
+    font-weight: bold;
+}
diff --git a/doc/sphinx/_static/coqnotations.sty b/doc/sphinx/_static/coqnotations.sty
new file mode 100644
index 0000000000..75eac1f724
--- /dev/null
+++ b/doc/sphinx/_static/coqnotations.sty
@@ -0,0 +1,50 @@
+% The LaTeX generator wraps all custom spans in \DUrole{class}{contents}.  That
+% command then checks for another command called \DUroleclass.
+
+% Most of our CSS class names have dashes, so we need ‘\csname … \endcsname’
+
+% <magic>
+% \def\newcssclass#1#2{\expandafter\def\csname DUrole#1\endcsname ##1{#2}}
+% </magic>
+
+\RequirePackage{adjustbox}
+\RequirePackage{xcolor}
+\RequirePackage{amsmath}
+
+\definecolor{nbordercolor}{HTML}{AAAAAA}
+\definecolor{nbgcolor}{HTML}{EAEAEA}
+\definecolor{nholecolor}{HTML}{4E9A06}
+
+\newlength{\nscriptsize}
+\setlength{\nscriptsize}{0.8em}
+
+\newcommand*{\scriptsmallsquarebox}[1]{%
+  % Force width
+  \makebox[\nscriptsize]{%
+    % Force height and center vertically
+    \raisebox{\dimexpr .5\nscriptsize - .5\height \relax}[\nscriptsize][0pt]{%
+      % Cancel depth
+      \raisebox{\depth}{#1}}}}
+\newcommand*{\nscriptdecoratedbox}[2][]{\adjustbox{cfbox=nbordercolor 0.5pt 0pt,bgcolor=nbgcolor}{#2}}
+\newcommand*{\nscriptbox}[1]{\nscriptdecoratedbox{\scriptsmallsquarebox{\textbf{#1}}}}
+\newcommand*{\nscript}[2]{\text{\hspace{-.5\nscriptsize}\raisebox{-#1\nscriptsize}{\nscriptbox{\small#2}}}}
+\newcommand*{\nsup}[1]{^{\nscript{0.15}{#1}}}
+\newcommand*{\nsub}[1]{_{\nscript{0.35}{#1}}}
+\newcommand*{\nnotation}[1]{#1}
+\newcommand*{\nrepeat}[1]{\text{\adjustbox{cfbox=nbordercolor 0.5pt 2pt,bgcolor=nbgcolor}{#1\hspace{.5\nscriptsize}}}}
+\newcommand*{\nwrapper}[1]{\ensuremath{\displaystyle#1}} % https://tex.stackexchange.com/questions/310877/
+\newcommand*{\nhole}[1]{\textit{\color{nholecolor}#1}}
+
+% <magic>
+% Make it easier to define new commands matching CSS classes
+\newcommand{\newcssclass}[2]{%
+  \expandafter\def\csname DUrole#1\endcsname##1{#2}
+}
+% </magic>
+
+\newcssclass{notation-sup}{\nsup{#1}}
+\newcssclass{notation-sub}{\nsub{#1}}
+\newcssclass{notation}{\nnotation{#1}}
+\newcssclass{repeat}{\nrepeat{#1}}
+\newcssclass{repeat-wrapper}{\nwrapper{#1}}
+\newcssclass{hole}{\nhole{#1}}
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
new file mode 100644
index 0000000000..1ae7a7cd7f
--- /dev/null
+++ b/doc/sphinx/_static/notations.css
@@ -0,0 +1,177 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+.notation {
+    /* font-family: "Ubuntu Mono", "Consolas", monospace; */
+    white-space: pre-wrap;
+}
+
+.notation .notation-sup {
+    top: -0.4em;
+}
+
+.notation .notation-sub {
+    bottom: -0.4em;
+    border-radius: 1rem;
+}
+
+@font-face { /* This font has been edited to center all characters */
+  font-family: 'UbuntuMono-Square';
+  font-style: normal;
+  font-weight: 800;
+  src: local('UbuntuMono-Square'), url(./UbuntuMono-Square.ttf) format('truetype');
+}
+
+.notation .notation-sup, .notation .notation-sub {
+    background: #EAEAEA;
+    border: 1px solid #AAA;
+    color: black;
+    /* cursor: help; */
+    display: inline-block;
+    font-size: 0.5em;
+    font-weight: bolder;
+    font-family: UbuntuMono-Square, monospace;
+    height: 2em;
+    line-height: 1.6em;
+    position: absolute;
+    right: -1em; /* half of the width */
+    text-align: center;
+    width: 2em;
+}
+
+.notation .repeat {
+    background: #EAEAEA;
+    border: 1px solid #AAA;
+    display: inline-block;
+    padding-right: 0.6em; /* Space for the left half of the sub- and sup-scripts */
+    padding-left: 0.2em;
+    margin: 0.25em 0;
+}
+
+.notation .repeat-wrapper {
+    display: inline-block;
+    position: relative;
+    margin-right: 0.4em; /* Space for the right half of the sub- and sup-scripts */
+}
+
+.notation .hole {
+    color: #4e9a06;
+    font-style: italic;
+}
+
+/***********************/
+/* Small extra classes */
+/***********************/
+
+.math-preamble {
+    display: none;
+}
+
+.inline-grammar-production {
+    font-weight: bold;
+}
+
+/************************/
+/* Coqtop IO and Coqdoc */
+/************************/
+
+.coqtop dd, .ansi-bg-default {
+    background: #eeeeee !important;
+}
+
+.coqtop dd, .ansi-fg-default {
+    color: #2e3436 !important;
+}
+
+.coqtop dt {                    /* Questions */
+    background: none !important;
+    color: #333 !important;
+    font-weight: normal !important;
+    padding: 0 !important;
+    margin: 0 !important;
+}
+
+.coqtop dd {                    /* Responses */
+    padding: 0.5em;
+    margin-left: 0 !important;
+    margin-top: 0.5em !important;
+}
+
+.coqdoc, .coqtop dl {
+    margin: 12px; /* Copied from RTD theme */
+}
+
+.coqdoc {
+    display: block;
+    white-space: pre;
+}
+
+.coqtop dt, .coqtop dd {
+    border: none !important;
+    display: block !important;
+}
+
+.coqtop.coqtop-hidden, dd.coqtop-hidden, dt.coqtop-hidden { /* Overqualifying for precedence */
+    display: none !important;
+}
+
+/* FIXME: Specific to the RTD theme */
+.coqdoc, .coqtop dt, .coqtop dd, pre { /* pre added because of production lists */
+    font-family: Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace !important; /* Copied from RTD theme */
+    font-size: 12px !important; /* Copied from RTD theme */
+    line-height: 1.5 !important; /* Copied from RTD theme */
+    white-space: pre;
+}
+
+/*************/
+/* Overrides */
+/*************/
+
+.rst-content table.docutils td, .rst-content table.docutils th {
+    padding: 8px; /* Reduce horizontal padding */
+    border-left: none;
+    border-right: none;
+}
+
+/* We can't display nested blocks otherwise */
+code, .rst-content tt, .rst-content code {
+    background: transparent !important;
+    border: none !important;
+    font-size: inherit !important;
+}
+
+code {
+    padding: 0 !important;      /* This padding doesn't make sense without a border */
+}
+
+dt > .property {
+    margin-right: 0.25em;
+}
+
+.icon-home:visited {
+  color: #FFFFFF;
+}
+
+/* FIXME: Specific to the RTD theme */
+a:visited {
+    color: #2980B9;
+}
+
+/* Pygments for Coq is confused by ‘…’ */
+code span.error {
+    background: inherit !important;
+    line-height: inherit !important;
+    margin-bottom: 0 !important;
+    padding: 0 !important;
+}
+
+/* Red is too aggressive */
+.rst-content tt.literal, .rst-content tt.literal, .rst-content code.literal {
+    color: inherit !important;
+}
diff --git a/doc/sphinx/_static/notations.js b/doc/sphinx/_static/notations.js
new file mode 100644
index 0000000000..eb7f211e8b
--- /dev/null
+++ b/doc/sphinx/_static/notations.js
@@ -0,0 +1,43 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+function annotateSup(marker) {
+    switch (marker) {
+    case "?":
+        return "This block is optional.";
+    case "*":
+        return "This block is optional, and may be repeated.";
+    case "+":
+        return "This block may be repeated.";
+    }
+}
+
+function annotateSub(separator) {
+    return "Use “" + separator + "” to separate repetitions of this block.";
+}
+
+// function translatePunctuation(original) {
+//     var mappings = { ",": "⸴" }; // ，
+//     return mappings[original] || original;
+// }
+
+function annotateNotations () {
+    $(".repeat-wrapper > sup")
+        .attr("data-hint", function() {
+            return annotateSup($(this).text());
+        }).addClass("hint--top hint--rounded");
+
+    $(".repeat-wrapper > sub")
+        .attr("data-hint", function() {
+            return annotateSub($(this).text());
+        }).addClass("hint--bottom hint--rounded");
+    //.text(function(i, text) { return translatePunctuation(text); });
+}
+
+$(annotateNotations);
diff --git a/doc/sphinx/_static/pre-text.css b/doc/sphinx/_static/pre-text.css
new file mode 100644
index 0000000000..38d81abefe
--- /dev/null
+++ b/doc/sphinx/_static/pre-text.css
@@ -0,0 +1,29 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+/* Formatting for PRE (literal) text in .rst files */
+
+.line-block {
+    background-color: rgb(80%,90%,80%);
+    margin: 0px;
+    margin-top: 0px;
+    margin-right: 16px;
+    margin-bottom: 20px;
+    padding-left: 4px;
+    padding-top: 4px;
+    padding-bottom: 4px;
+}
+
+.line-block cite {
+    font-size: 90%;
+}
+
+.pre {
+    font-size: 90%;
+}
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
new file mode 100755
index 0000000000..0bff41a259
--- /dev/null
+++ b/doc/sphinx/conf.py
@@ -0,0 +1,400 @@
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+##########################################################################
+##         #   The Coq Proof Assistant / The Coq Development Team       ##
+##  v      #   INRIA, CNRS and contributors - Copyright 1999-2018       ##
+## <O___,, #       (see CREDITS file for the list of authors)           ##
+##   \VV/  ###############################################################
+##    //   #    This file is distributed under the terms of the         ##
+##         #     GNU Lesser General Public License Version 2.1          ##
+##         #     (see LICENSE file for the text of the license)         ##
+##########################################################################
+#
+# Coq 8.5 documentation build configuration file, created by
+# sphinx-quickstart on Wed May 11 11:23:13 2016.
+#
+# This file is execfile()d with the current directory set to its
+# containing dir.
+#
+# Note that not all possible configuration values are present in this
+# autogenerated file.
+#
+# All configuration values have a default; values that are commented out
+# serve to show the default.
+
+import sys
+import os
+
+# Increase recursion limit for sphinx
+sys.setrecursionlimit(1500)
+
+# If extensions (or modules to document with autodoc) are in another directory,
+# add these directories to sys.path here. If the directory is relative to the
+# documentation root, use os.path.abspath to make it absolute, like shown here.
+sys.path.append(os.path.abspath('../tools/'))
+
+# -- General configuration ------------------------------------------------
+
+# If your documentation needs a minimal Sphinx version, state it here.
+#needs_sphinx = '1.0'
+
+# Add any Sphinx extension module names here, as strings. They can be
+# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
+# ones.
+extensions = [
+    'sphinx.ext.mathjax',
+    'sphinx.ext.todo',
+    'sphinxcontrib.bibtex',
+    'coqrst.coqdomain'
+]
+
+# Add any paths that contain templates here, relative to this directory.
+templates_path = ['_templates']
+
+# The suffix(es) of source filenames.
+# You can specify multiple suffix as a list of string:
+# source_suffix = ['.rst', '.md']
+source_suffix = '.rst'
+
+# The encoding of source files.
+#source_encoding = 'utf-8-sig'
+
+# The master toctree document.
+master_doc = 'index'
+
+# General information about the project.
+project = 'Coq'
+copyright = '2016, Inria'
+author = 'The Coq Development Team'
+
+# The version info for the project you're documenting, acts as replacement for
+# |version| and |release|, also used in various other places throughout the
+# built documents.
+#
+# The short X.Y version.
+version = '8.7'
+# The full version, including alpha/beta/rc tags.
+release = '8.7.dev'
+
+# The language for content autogenerated by Sphinx. Refer to documentation
+# for a list of supported languages.
+#
+# This is also used if you do content translation via gettext catalogs.
+# Usually you set "language" from the command line for these cases.
+language = None
+
+# There are two options for replacing |today|: either, you set today to some
+# non-false value, then it is used:
+#today = ''
+# Else, today_fmt is used as the format for a strftime call.
+#today_fmt = '%B %d, %Y'
+
+# List of patterns, relative to source directory, that match files and
+# directories to ignore when looking for source files.
+# This patterns also effect to html_static_path and html_extra_path
+exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store']
+
+# The reST default role (used for this markup: `text`) to use for all
+# documents.
+#default_role = None
+
+# Use the Coq domain
+primary_domain = 'coq'
+
+# If true, '()' will be appended to :func: etc. cross-reference text.
+#add_function_parentheses = True
+
+# If true, the current module name will be prepended to all description
+# unit titles (such as .. function::).
+#add_module_names = True
+
+# If true, sectionauthor and moduleauthor directives will be shown in the
+# output. They are ignored by default.
+#show_authors = False
+
+# The name of the Pygments (syntax highlighting) style to use.
+pygments_style = 'sphinx'
+highlight_language = 'text'
+
+# A list of ignored prefixes for module index sorting.
+#modindex_common_prefix = []
+
+# If true, keep warnings as "system message" paragraphs in the built documents.
+#keep_warnings = False
+
+# If true, `todo` and `todoList` produce output, else they produce nothing.
+todo_include_todos = False
+
+# Extra warnings, including undefined references
+nitpicky = False
+
+# -- Options for HTML output ----------------------------------------------
+
+# The theme to use for HTML and HTML Help pages.  See the documentation for
+# a list of builtin themes.
+html_theme = 'sphinx_rtd_theme'
+# html_theme = 'agogo'
+# html_theme = 'alabaster'
+# html_theme = 'haiku'
+# html_theme = 'bizstyle'
+
+# Theme options are theme-specific and customize the look and feel of a theme
+# further.  For a list of options available for each theme, see the
+# documentation.
+#html_theme_options = {}
+
+# Add any paths that contain custom themes here, relative to this directory.
+import sphinx_rtd_theme
+html_theme_path = [sphinx_rtd_theme.get_html_theme_path()]
+
+# The name for this set of Sphinx documents.
+# "<project> v<release> documentation" by default.
+#html_title = 'Coq 8.5 v8.5pl1'
+
+# A shorter title for the navigation bar.  Default is the same as html_title.
+#html_short_title = None
+
+# The name of an image file (relative to this directory) to place at the top
+# of the sidebar.
+#html_logo = None
+
+# The name of an image file (relative to this directory) to use as a favicon of
+# the docs.  This file should be a Windows icon file (.ico) being 16x16 or 32x32
+# pixels large.
+#html_favicon = None
+
+# Add any paths that contain custom static files (such as style sheets) here,
+# relative to this directory. They are copied after the builtin static files,
+# so a file named "default.css" will overwrite the builtin "default.css".
+html_static_path = ['_static']
+
+# Add any extra paths that contain custom files (such as robots.txt or
+# .htaccess) here, relative to this directory. These files are copied
+# directly to the root of the documentation.
+#html_extra_path = []
+
+# If not None, a 'Last updated on:' timestamp is inserted at every page
+# bottom, using the given strftime format.
+# The empty string is equivalent to '%b %d, %Y'.
+#html_last_updated_fmt = None
+
+# If true, SmartyPants will be used to convert quotes and dashes to
+# typographically correct entities.
+html_use_smartypants = False # FIXME wrap code in <code> tags, otherwise quotesget converted in there
+
+# Custom sidebar templates, maps document names to template names.
+#html_sidebars = {}
+
+# Additional templates that should be rendered to pages, maps page names to
+# template names.
+#html_additional_pages = {}
+
+# If false, no module index is generated.
+#html_domain_indices = True
+
+# If false, no index is generated.
+#html_use_index = True
+
+# If true, the index is split into individual pages for each letter.
+#html_split_index = False
+
+# If true, links to the reST sources are added to the pages.
+#html_show_sourcelink = True
+
+# If true, "Created using Sphinx" is shown in the HTML footer. Default is True.
+#html_show_sphinx = True
+
+# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True.
+#html_show_copyright = True
+
+# If true, an OpenSearch description file will be output, and all pages will
+# contain a <link> tag referring to it.  The value of this option must be the
+# base URL from which the finished HTML is served.
+#html_use_opensearch = ''
+
+# This is the file name suffix for HTML files (e.g. ".xhtml").
+#html_file_suffix = None
+
+# Language to be used for generating the HTML full-text search index.
+# Sphinx supports the following languages:
+#   'da', 'de', 'en', 'es', 'fi', 'fr', 'h', 'it', 'ja'
+#   'nl', 'no', 'pt', 'ro', 'r', 'sv', 'tr', 'zh'
+#html_search_language = 'en'
+
+# A dictionary with options for the search language support, empty by default.
+# 'ja' uses this config value.
+# 'zh' user can custom change `jieba` dictionary path.
+#html_search_options = {'type': 'default'}
+
+# The name of a javascript file (relative to the configuration directory) that
+# implements a search results scorer. If empty, the default will be used.
+#html_search_scorer = 'scorer.js'
+
+# Output file base name for HTML help builder.
+htmlhelp_basename = 'Coq85doc'
+
+# -- Options for LaTeX output ---------------------------------------------
+
+###########################
+# Set things up for XeTeX #
+###########################
+latex_elements = {
+    'babel': '',
+    'fontenc': '',
+    'inputenc': '',
+    'utf8extra': '',
+    'cmappkg': '',
+    # https://www.topbug.net/blog/2015/12/10/a-collection-of-issues-about-the-latex-output-in-sphinx-and-the-solutions/
+    'papersize': 'letterpaper',
+    'classoptions': ',openany', # No blank pages
+    'polyglossia' : '\\usepackage{polyglossia}',
+    'unicode-math' : '\\usepackage{unicode-math}',
+    'microtype' : '\\usepackage{microtype}',
+    "preamble": r"\usepackage{coqnotations}"
+}
+
+from sphinx.builders.latex import LaTeXBuilder
+
+########
+# done #
+########
+
+latex_additional_files = ["_static/coqnotations.sty"]
+
+# Grouping the document tree into LaTeX files. List of tuples
+# (source start file, target name, title,
+#  author, documentclass [howto, manual, or own class]).
+latex_documents = [
+    (master_doc, 'Coq85.tex', 'Coq 8.5 Documentation',
+     'The Coq Development Team (edited by C. Pit-Claudel)', 'manual'),
+]
+
+# The name of an image file (relative to this directory) to place at the top of
+# the title page.
+#latex_logo = None
+
+# For "manual" documents, if this is true, then toplevel headings are parts,
+# not chapters.
+#latex_use_parts = False
+
+# If true, show page references after internal links.
+#latex_show_pagerefs = False
+
+# If true, show URL addresses after external links.
+#latex_show_urls = False
+
+# Documents to append as an appendix to all manuals.
+#latex_appendices = []
+
+# If false, no module index is generated.
+#latex_domain_indices = True
+
+
+# -- Options for manual page output ---------------------------------------
+
+# One entry per manual page. List of tuples
+# (source start file, name, description, authors, manual section).
+man_pages = [
+    (master_doc, 'coq85', 'Coq 8.5 Documentation',
+     [author], 1)
+]
+
+# If true, show URL addresses after external links.
+#man_show_urls = False
+
+
+# -- Options for Texinfo output -------------------------------------------
+
+# Grouping the document tree into Texinfo files. List of tuples
+# (source start file, target name, title, author,
+#  dir menu entry, description, category)
+texinfo_documents = [
+    (master_doc, 'Coq85', 'Coq 8.5 Documentation',
+     author, 'Coq85', 'One line description of project.',
+     'Miscellaneous'),
+]
+
+# Documents to append as an appendix to all manuals.
+#texinfo_appendices = []
+
+# If false, no module index is generated.
+#texinfo_domain_indices = True
+
+# How to display URL addresses: 'footnote', 'no', or 'inline'.
+#texinfo_show_urls = 'footnote'
+
+# If true, do not generate a @detailmenu in the "Top" node's menu.
+#texinfo_no_detailmenu = False
+
+
+# -- Options for Epub output ----------------------------------------------
+
+# Bibliographic Dublin Core info.
+epub_title = project
+epub_author = author
+epub_publisher = author
+epub_copyright = copyright
+
+# The basename for the epub file. It defaults to the project name.
+#epub_basename = project
+
+# The HTML theme for the epub output. Since the default themes are not
+# optimized for small screen space, using the same theme for HTML and epub
+# output is usually not wise. This defaults to 'epub', a theme designed to save
+# visual space.
+#epub_theme = 'epub'
+
+# The language of the text. It defaults to the language option
+# or 'en' if the language is not set.
+#epub_language = ''
+
+# The scheme of the identifier. Typical schemes are ISBN or URL.
+#epub_scheme = ''
+
+# The unique identifier of the text. This can be a ISBN number
+# or the project homepage.
+#epub_identifier = ''
+
+# A unique identification for the text.
+#epub_uid = ''
+
+# A tuple containing the cover image and cover page html template filenames.
+#epub_cover = ()
+
+# A sequence of (type, uri, title) tuples for the guide element of content.opf.
+#epub_guide = ()
+
+# HTML files that should be inserted before the pages created by sphinx.
+# The format is a list of tuples containing the path and title.
+#epub_pre_files = []
+
+# HTML files that should be inserted after the pages created by sphinx.
+# The format is a list of tuples containing the path and title.
+#epub_post_files = []
+
+# A list of files that should not be packed into the epub file.
+epub_exclude_files = ['search.html']
+
+# The depth of the table of contents in toc.ncx.
+#epub_tocdepth = 3
+
+# Allow duplicate toc entries.
+#epub_tocdup = True
+
+# Choose between 'default' and 'includehidden'.
+#epub_tocscope = 'default'
+
+# Fix unsupported image types using the Pillow.
+#epub_fix_images = False
+
+# Scale large images.
+#epub_max_image_width = 0
+
+# How to display URL addresses: 'footnote', 'no', or 'inline'.
+#epub_show_urls = 'inline'
+
+# If false, no index is generated.
+#epub_use_index = True
+
+# navtree options
+navtree_shift = True
diff --git a/doc/sphinx/coqdoc.css b/doc/sphinx/coqdoc.css
new file mode 100644
index 0000000000..a34bb81ebd
--- /dev/null
+++ b/doc/sphinx/coqdoc.css
@@ -0,0 +1,338 @@
+/************************************************************************/
+/*         *   The Coq Proof Assistant / The Coq Development Team       */
+/*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       */
+/* <O___,, *       (see CREDITS file for the list of authors)           */
+/*   \VV/  **************************************************************/
+/*    //   *    This file is distributed under the terms of the         */
+/*         *     GNU Lesser General Public License Version 2.1          */
+/*         *     (see LICENSE file for the text of the license)         */
+/************************************************************************/
+body { padding: 0px 0px;
+       margin: 0px 0px;
+       background-color: white }
+
+#page { display: block;
+        padding: 0px;
+        margin: 0px;
+        padding-bottom: 10px; }
+
+#header { display: block;
+          position: relative;
+          padding: 0;
+          margin: 0;
+          vertical-align: middle;
+          border-bottom-style: solid;
+          border-width: thin }
+
+#header h1 { padding: 0;
+             margin: 0;}
+
+
+/* Contents */
+
+#main{ display: block;
+       padding: 10px;
+       font-family: sans-serif;
+       font-size: 100%;
+       line-height: 100% }
+
+#main  h1 { line-height: 95% } /* allow for multi-line headers */
+
+#main  a.idref:visited {color : #416DFF; text-decoration : none; }
+#main  a.idref:link {color : #416DFF; text-decoration : none; }
+#main  a.idref:hover {text-decoration : none; }
+#main  a.idref:active {text-decoration : none; }
+
+#main  a.modref:visited {color : #416DFF; text-decoration : none; }
+#main  a.modref:link {color : #416DFF; text-decoration : none; }
+#main  a.modref:hover {text-decoration : none; }
+#main  a.modref:active {text-decoration : none; }
+
+#main .keyword { color : #cf1d1d }
+#main { color: black }
+
+.section { background-color: rgb(60%,60%,100%);
+           padding-top: 13px;
+           padding-bottom: 13px;
+           padding-left: 3px;
+           margin-top: 5px;
+           margin-bottom: 5px;
+           font-size : 175% }
+
+h2.section { background-color: rgb(80%,80%,100%);
+             padding-left: 3px;
+             padding-top: 12px;
+             padding-bottom: 10px;
+             font-size : 130% }
+
+h3.section { background-color: rgb(90%,90%,100%);
+             padding-left: 3px;
+             padding-top: 7px;
+             padding-bottom: 7px;
+             font-size : 115% }
+
+h4.section {
+/*
+                   background-color: rgb(80%,80%,80%);
+                   max-width: 20em;
+                   padding-left: 5px;
+                   padding-top: 5px;
+                   padding-bottom: 5px;
+*/
+                   background-color: white;
+                   padding-left: 0px;
+                   padding-top: 0px;
+                   padding-bottom: 0px;
+                   font-size : 100%;
+                   font-weight : bold;
+                   text-decoration : underline;
+ }
+
+#main .doc { margin: 0px;
+             font-family: sans-serif;
+             font-size: 100%;
+             line-height: 125%;
+             max-width: 40em;
+             color: black;
+             padding: 10px;
+             background-color: #90bdff }
+
+.inlinecode {
+    display: inline;
+/*    font-size: 125%; */
+    color: #666666;
+    font-family: monospace }
+
+.doc .inlinecode {
+    display: inline;
+    font-size: 120%;
+    color: rgb(30%,30%,70%);
+    font-family: monospace }
+
+.doc .inlinecode .id {
+    color: rgb(30%,30%,70%);
+}
+
+.inlinecodenm {
+    display: inline;
+    color: #444444;
+}
+
+.doc .code {
+    display: inline;
+    font-size: 120%;
+    color: rgb(30%,30%,70%);
+    font-family: monospace }
+
+.comment {
+    display: inline;
+    font-family: monospace;
+    color: rgb(50%,50%,80%);
+}
+
+.code {
+    display: block;
+/*  padding-left: 15px; */
+    font-size: 110%;
+    font-family: monospace;
+ }
+
+table.infrule {
+  border: 0px;
+  margin-left: 50px;
+  margin-top: 10px;
+  margin-bottom: 10px;
+}
+
+td.infrule {
+    font-family: monospace;
+    text-align: center;
+/*    color: rgb(35%,35%,70%);  */
+    padding: 0px;
+    line-height: 100%;
+}
+
+tr.infrulemiddle hr {
+    margin: 1px 0 1px 0;
+}
+
+.infrulenamecol {
+    color: rgb(60%,60%,60%);
+    font-size: 80%;
+    padding-left: 1em;
+    padding-bottom: 0.1em
+}
+
+/* Pied de page */
+
+#footer { font-size: 65%;
+          font-family: sans-serif; }
+
+/* Identifiers: <span class="id" title="...">) */
+
+.id { display: inline; }
+
+.id[title="constructor"] {
+    color: rgb(60%,0%,0%);
+}
+
+.id[title="var"] {
+    color: rgb(40%,0%,40%);
+}
+
+.id[title="variable"] {
+    color: rgb(40%,0%,40%);
+}
+
+.id[title="definition"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="abbreviation"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="lemma"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="instance"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="projection"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="method"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="inductive"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="record"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="class"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="keyword"] {
+ color : #cf1d1d;
+/*     color: black; */
+}
+
+/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */
+
+.id[type="constructor"] {
+    color: rgb(60%,0%,0%);
+}
+
+.id[type="var"] {
+    color: rgb(40%,0%,40%);
+}
+
+.id[type="variable"] {
+    color: rgb(40%,0%,40%);
+}
+
+.id[type="definition"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="abbreviation"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="lemma"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="instance"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="projection"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="method"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[type="inductive"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[type="record"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[type="class"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[type="keyword"] {
+ color : #cf1d1d;
+/*     color: black; */
+}
+
+.inlinecode .id {
+    color: rgb(0%,0%,0%);
+}
+
+
+/* TOC */
+
+#toc h2 {
+    padding: 10px;
+    background-color: rgb(60%,60%,100%);
+}
+
+#toc li {
+    padding-bottom: 8px;
+}
+
+/* Index */
+
+#index {
+    margin: 0;
+    padding: 0;
+    width: 100%;
+}
+
+#index #frontispiece {
+    margin: 1em auto;
+    padding: 1em;
+    width: 60%;
+}
+
+.booktitle { font-size : 140%  }
+.authors { font-size : 90%;
+                 line-height: 115%;  }
+.moreauthors { font-size : 60%  }
+
+#index #entrance {
+    text-align: center;
+}
+
+#index #entrance .spacer {
+    margin: 0 30px 0 30px;
+}
+
+#index #footer {
+    position: absolute;
+    bottom: 0;
+}
+
+.paragraph {
+    height: 0.75em;
+}
+
+ul.doclist {
+    margin-top: 0em;
+    margin-bottom: 0em;
+}
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/doc/sphinx/index.rst