Imported Upstream version 8.8.2upstream/8.8.2

26 files changed, 2790 insertions, 91 deletions

diff --git a/doc/LICENSE b/doc/LICENSE
index ada22e66..c223a4e1 100644
--- a/doc/LICENSE
+++ b/doc/LICENSE
@@ -2,11 +2,17 @@ The Coq Reference Manual is a collective work from the Coq Development
 Team whose members are listed in the file CREDITS of the Coq source
 package. All related documents (the LaTeX and BibTeX sources, the
 embedded png files, and the PostScript, PDF and html outputs) are
-copyright (c) INRIA 1999-2006. The material connected to the Reference
-Manual may be distributed only subject to the terms and conditions set
-forth in the Open Publication License, v1.0 or later (the latest
-version is presently available at http://www.opencontent.org/openpub/).
-Options A and B are *not* elected.
+copyright (c) INRIA 1999-2006, with the exception of the Ubuntu font
+file UbuntuMono-B.ttf, which is
+Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font
+license, version 1.0
+(https://www.ubuntu.com/legal/terms-and-policies/font-licence), and its
+derivative CoqNotations.ttf distributed under the same license. The
+material connected to the Reference Manual may be distributed only
+subject to the terms and conditions set forth in the Open Publication
+License, v1.0 or later (the latest version is presently available at
+http://www.opencontent.org/openpub/).  Options A and B are *not*
+elected.
 
 The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine
 Paulin-Mohring. All documents (the LaTeX source and the PostScript,
@@ -25,16 +31,6 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA
 distributed under the terms of the Lesser General Public License
 version 2.1 or later. 
 
-The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo
-Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All
-documents (the LaTeX source and the PostScript, PDF and html outputs)
-are copyright (c) INRIA 2004-2006. The material connected to the FAQ
-(Coq for the Clueless) may be distributed only subject to the terms
-and conditions set forth in the Open Publication License, v1.0 or
-later (the latest version is presently available at
-http://www.opencontent.org/openpub/). Options A and B are *not*
-elected.
-
 The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre
 Castéran and Eduardo Gimenez. All related documents (the LaTeX and
 BibTeX sources and the PostScript, PDF and html outputs) are copyright
diff --git a/doc/Makefile.rt b/doc/Makefile.rt
deleted file mode 100644
index 6c328134..00000000
--- a/doc/Makefile.rt
+++ /dev/null
@@ -1,43 +0,0 @@
-# Makefile for building Coq Technical Reports
-
-# if coqc,coqtop,coq-tex are not in your PATH, you need the environment 
-# variable COQBIN to be correctly set  
-# (COQTOP is autodetected)
-# (some files are preprocessed using Coq and some part of the documentation
-# is automatically built from the theories sources)
-
-# To compile documentation, you need the following tools:
-# Dvi: latex (latex2e), bibtex, makeindex, dviselect (package RPM dviutils)
-# Ps: dvips, psutils (ftp://ftp.dcs.ed.ac.uk/pub/ajcd/psutils.tar.gz)
-# Pdf: pdflatex
-# Html:
-#   - hevea: http://para.inria.fr/~maranget/hevea/
-#   - htmlSplit: http://coq.inria.fr/~delahaye
-# Rapports INRIA: dviselect, rrkit (par Michel Mauny)
-
-include ./Makefile
-
-###################
-# RT
-###################
-# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny)
-rt/Reference-Manual-RT.dvi: refman/Reference-Manual.dvi rt/RefMan-cover.tex
-	dviselect -i refman/Reference-Manual.dvi -o rt/RefMan-body.dvi 3:
-	(cd rt; $(LATEX) RefMan-cover.tex)
-	set a=`tail -1 refman/Reference-Manual.log`;\
-	set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\
-	(cd rt; if $(TEST) "$$a = 0";\
-	 then rrkit  RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\
-	 else rrkit -odd RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\
-	fi)
-
-# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny)
-rt/Tutorial-RT.dvi : tutorial/Tutorial.v.dvi rt/Tutorial-cover.tex
-	dviselect -i rt/Tutorial.v.dvi -o rt/Tutorial-body.dvi 3:
-	(cd rt; $(LATEX) Tutorial-cover.tex)
-	set a=`tail -1 tutorial/Tutorial.v.log`;\
-	set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\
-	(cd rt; if $(TEST) "$$a = 0";\
-	 then rrkit      Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\
-	 else rrkit -odd Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\
-	fi)
diff --git a/doc/common/styles/html/simple/style.css b/doc/common/styles/html/simple/style.css
index 0b1e640b..d1b2ce11 100644
--- a/doc/common/styles/html/simple/style.css
+++ b/doc/common/styles/html/simple/style.css
@@ -10,4 +10,4 @@
     margin: 0pt;
     padding: .5ex 1em;
     list-style: none 
-}
\ No newline at end of file
+}
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 9216c81f..8c09b23a 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -18,6 +18,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Init/Logic.v
     theories/Init/Logic_Type.v
     theories/Init/Nat.v
+    theories/Init/Decimal.v
     theories/Init/Peano.v
     theories/Init/Specif.v
     theories/Init/Tactics.v
@@ -46,6 +47,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/ClassicalDescription.v
     theories/Logic/ClassicalEpsilon.v
     theories/Logic/ClassicalUniqueChoice.v
+    theories/Logic/SetoidChoice.v
     theories/Logic/Berardi.v
     theories/Logic/Diaconescu.v
     theories/Logic/Hurkens.v
@@ -55,7 +57,10 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/Description.v
     theories/Logic/Epsilon.v
     theories/Logic/IndefiniteDescription.v
+    theories/Logic/PropExtensionality.v
+    theories/Logic/PropExtensionalityFacts.v
     theories/Logic/FunctionalExtensionality.v
+    theories/Logic/ExtensionalFunctionRepresentative.v
     theories/Logic/ExtensionalityFacts.v
     theories/Logic/WeakFan.v
     theories/Logic/WKL.v
@@ -220,8 +225,13 @@ through the <tt>Require Import</tt> command.</p>
     <dd>
     theories/Numbers/BinNums.v
     theories/Numbers/NumPrelude.v
-    theories/Numbers/BigNumPrelude.v
     theories/Numbers/NaryFunctions.v
+    theories/Numbers/DecimalFacts.v
+    theories/Numbers/DecimalNat.v
+    theories/Numbers/DecimalPos.v
+    theories/Numbers/DecimalN.v
+    theories/Numbers/DecimalZ.v
+    theories/Numbers/DecimalString.v
     </dd>
 
     <dt> <b>&nbsp;&nbsp;NatInt</b>:
@@ -252,16 +262,7 @@ through the <tt>Require Import</tt> command.</p>
     <dd>
     theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
     theories/Numbers/Cyclic/Abstract/NZCyclic.v
-    theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
-    theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
-    theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
-    theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
-    theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
-    theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
-    theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
-    theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
-    theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
-    theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+    theories/Numbers/Cyclic/Abstract/DoubleType.v
     theories/Numbers/Cyclic/Int31/Cyclic31.v
     theories/Numbers/Cyclic/Int31/Ring31.v
     theories/Numbers/Cyclic/Int31/Int31.v
@@ -294,12 +295,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Natural/Abstract/NProperties.v
     theories/Numbers/Natural/Binary/NBinary.v
     theories/Numbers/Natural/Peano/NPeano.v
-    theories/Numbers/Natural/SpecViaZ/NSig.v
-    theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
-    theories/Numbers/Natural/BigN/BigN.v
-    theories/Numbers/Natural/BigN/Nbasic.v
-    theories/Numbers/Natural/BigN/NMake.v
-    theories/Numbers/Natural/BigN/NMake_gen.v
     </dd>
 
     <dt> <b>&nbsp;&nbsp;Integer</b>:
@@ -327,19 +322,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Integer/Abstract/ZDivTrunc.v
     theories/Numbers/Integer/Binary/ZBinary.v
     theories/Numbers/Integer/NatPairs/ZNatPairs.v
-    theories/Numbers/Integer/SpecViaZ/ZSig.v
-    theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
-    theories/Numbers/Integer/BigZ/BigZ.v
-    theories/Numbers/Integer/BigZ/ZMake.v
-    </dd>
-
-    <dt><b>&nbsp;&nbsp;Rational</b>:
-       Abstract and 31-bits-words-based rational arithmetic
-    </dt>
-    <dd>
-    theories/Numbers/Rational/SpecViaQ/QSig.v
-    theories/Numbers/Rational/BigQ/BigQ.v
-    theories/Numbers/Rational/BigQ/QMake.v
     </dd>
     </dl>
   </dd>
@@ -614,8 +596,8 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq84.v
-    theories/Compat/Coq85.v
     theories/Compat/Coq86.v
+    theories/Compat/Coq87.v
+    theories/Compat/Coq88.v
   </dd>
 </dl>
diff --git a/doc/tools/coqrst/__init__.py b/doc/tools/coqrst/__init__.py
new file mode 100644
index 00000000..2dda7d92
--- /dev/null
+++ b/doc/tools/coqrst/__init__.py
@@ -0,0 +1,10 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+"""Utilities for documenting Coq in Sphinx"""
diff --git a/doc/tools/coqrst/checkdeps.py b/doc/tools/coqrst/checkdeps.py
new file mode 100644
index 00000000..11f95c4e
--- /dev/null
+++ b/doc/tools/coqrst/checkdeps.py
@@ -0,0 +1,39 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+from __future__ import print_function
+import sys
+
+def eprint(*args, **kwargs):
+    print(*args, file=sys.stderr, **kwargs)
+
+def missing_dep(dep):
+    eprint('Cannot find %s (needed to build documentation)' % dep)
+    eprint('You can run `pip3 install %s` to install it.' % dep)
+    sys.exit(1)
+
+try:
+    import sphinx_rtd_theme
+except:
+    missing_dep('sphinx_rtd_theme')
+
+try:
+    import pexpect
+except:
+    missing_dep('pexpect')
+
+try:
+    import antlr4
+except:
+    missing_dep('antlr4-python3-runtime')
+
+try:
+    import bs4
+except:
+    missing_dep('beautifulsoup4')
diff --git a/doc/tools/coqrst/coqdoc/__init__.py b/doc/tools/coqrst/coqdoc/__init__.py
new file mode 100644
index 00000000..a89a548e
--- /dev/null
+++ b/doc/tools/coqrst/coqdoc/__init__.py
@@ -0,0 +1,10 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+from .main import *
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py
new file mode 100644
index 00000000..57adcb28
--- /dev/null
+++ b/doc/tools/coqrst/coqdoc/main.py
@@ -0,0 +1,91 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+"""
+Use CoqDoc to highlight Coq snippets
+====================================
+
+Pygment's Coq parser isn't the best; instead, use coqdoc to highlight snippets.
+Only works for full, syntactically valid sentences; on shorter snippets, coqdoc
+swallows parts of the input.
+
+Works by reparsing coqdoc's output into the output that Sphinx expects from a
+lexer.
+"""
+
+import os
+import platform
+from tempfile import mkstemp
+from subprocess import check_output
+
+from bs4 import BeautifulSoup
+from bs4.element import NavigableString
+
+COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals',
+                  '-s', '--html', '--stdout', '--utf8']
+
+COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"]
+COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS)
+
+def coqdoc(coq_code, coqdoc_bin=None):
+    """Get the output of coqdoc on coq_code."""
+    coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc")
+    fd, filename = mkstemp(prefix="coqdoc-", suffix=".v")
+    if platform.system().startswith("CYGWIN"):
+        # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..."
+        filename = check_output(["cygpath", "-w", filename]).decode("utf-8").strip()
+    try:
+        os.write(fd, COQDOC_HEADER.encode("utf-8"))
+        os.write(fd, coq_code.encode("utf-8"))
+        os.close(fd)
+        return check_output([coqdoc_bin] + COQDOC_OPTIONS + [filename], timeout = 10).decode("utf-8")
+    finally:
+        os.remove(filename)
+
+def is_whitespace_string(elem):
+    return isinstance(elem, NavigableString) and elem.strip() == ""
+
+def strip_soup(soup, pred):
+    """Strip elements maching pred from front and tail of soup."""
+    while soup.contents and pred(soup.contents[-1]):
+        soup.contents.pop()
+
+    skip = 0
+    for elem in soup.contents:
+        if not pred(elem):
+            break
+        skip += 1
+
+    soup.contents[:] = soup.contents[skip:]
+
+def lex(source):
+    """Convert source into a stream of (css_classes, token_string)."""
+    coqdoc_output = coqdoc(source)
+    soup = BeautifulSoup(coqdoc_output, "html.parser")
+    root = soup.find(class_='code')
+    strip_soup(root, is_whitespace_string)
+    for elem in root.children:
+        if isinstance(elem, NavigableString):
+            yield [], elem
+        elif elem.name == "span":
+            cls = "coqdoc-{}".format(elem['title'])
+            yield [cls], elem.string
+        elif elem.name == 'br':
+            pass
+        else:
+            raise ValueError(elem)
+
+def main():
+    """Lex stdin (for testing purposes)"""
+    import sys
+    for classes, text in lex(sys.stdin.read()):
+        print(repr(text) + "\t" ' '.join(classes))
+
+if __name__ == '__main__':
+    main()
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
new file mode 100644
index 00000000..edf4e6ec
--- /dev/null
+++ b/doc/tools/coqrst/coqdomain.py
@@ -0,0 +1,1201 @@
+# -*- 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)         ##
+##########################################################################
+"""A Coq domain for Sphinx.
+
+Currently geared towards Coq's manual, rather than Coq source files, but one
+could imagine extending it.
+"""
+
+# pylint: disable=too-few-public-methods
+
+import re
+from itertools import chain
+from collections import defaultdict
+
+from docutils import nodes, utils
+from docutils.transforms import Transform
+from docutils.parsers.rst import Directive, directives
+from docutils.parsers.rst.roles import code_role #, set_classes
+from docutils.parsers.rst.directives.admonitions import BaseAdmonition
+
+from sphinx import addnodes
+from sphinx.roles import XRefRole
+from sphinx.errors import ExtensionError
+from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode
+from sphinx.util.logging import getLogger
+from sphinx.directives import ObjectDescription
+from sphinx.domains import Domain, ObjType, Index
+from sphinx.domains.std import token_xrefs
+from sphinx.ext import mathbase
+
+from . import coqdoc
+from .repl import ansicolors
+from .repl.coqtop import CoqTop
+from .notations.sphinx import sphinxify
+from .notations.plain import stringify_with_ellipses
+
+def parse_notation(notation, source, line, rawtext=None):
+    """Parse notation and wrap it in an inline node"""
+    node = nodes.inline(rawtext or notation, '', *sphinxify(notation), classes=['notation'])
+    node.source, node.line = source, line
+    return node
+
+def highlight_using_coqdoc(sentence):
+    """Lex sentence using coqdoc, and yield inline nodes for each token"""
+    tokens = coqdoc.lex(utils.unescape(sentence, 1))
+    for classes, value in tokens:
+        yield nodes.inline(value, value, classes=classes)
+
+def make_target(objtype, targetid):
+    """Create a target to an object of type objtype and id targetid"""
+    return "coq:{}.{}".format(objtype, targetid)
+
+def make_math_node(latex, docname, nowrap):
+    node = mathbase.displaymath()
+    node['latex'] = latex
+    node['label'] = None # Otherwise equations are numbered
+    node['nowrap'] = nowrap
+    node['docname'] = docname
+    node['number'] = None
+    return node
+
+class CoqObject(ObjectDescription):
+    """A generic Coq object for Sphinx; all Coq objects are subclasses of this.
+
+    The fields and methods to override are listed at the top of this class'
+    implementation.  Each object supports the :name: option, which gives an
+    explicit name to link to.
+
+    See the comments and docstrings in CoqObject for more information.
+    """
+
+    # The semantic domain in which this object lives (eg. “tac”, “cmd”, “chm”…).
+    # It matches exactly one of the roles used for cross-referencing.
+    subdomain = None # type: str
+
+    # The suffix to use in indices for objects of this type (eg. “(tac)”)
+    index_suffix = None # type: str
+
+    # The annotation to add to headers of objects of this type
+    # (eg. “Command”, “Theorem”)
+    annotation = None # type: str
+
+    def _name_from_signature(self, signature): # pylint: disable=no-self-use, unused-argument
+        """Convert a signature into a name to link to.
+
+        ‘Signature’ is Sphinx parlance for an object's header (think “type
+        signature”); for example, the signature of the simplest form of the
+        ``exact`` tactic is ``exact @id``.
+
+        Returns None by default, in which case no name will be automatically
+        generated.  This is a convenient way to automatically generate names
+        (link targets) without having to write explicit names everywhere.
+
+        """
+        return None
+
+    def _render_signature(self, signature, signode):
+        """Render a signature, placing resulting nodes into signode."""
+        raise NotImplementedError(self)
+
+    option_spec = {
+        # Explicit object naming
+        'name': directives.unchanged,
+        # Silence warnings produced by report_undocumented_coq_objects
+        'undocumented': directives.flag,
+        # noindex omits this object from its index
+        'noindex': directives.flag
+    }
+
+    def subdomain_data(self):
+        if self.subdomain is None:
+            raise ValueError()
+        return self.env.domaindata['coq']['objects'][self.subdomain]
+
+    def _render_annotation(self, signode):
+        if self.annotation:
+            annot_node = nodes.inline(self.annotation, self.annotation, classes=['sigannot'])
+            signode += addnodes.desc_annotation(self.annotation, '', annot_node)
+            signode += nodes.Text(' ')
+
+    def handle_signature(self, signature, signode):
+        """Prefix signature with the proper annotation, then render it using
+        ``_render_signature`` (for example, add “Command” in front of commands).
+
+        :returns: the name given to the resulting node, if any
+        """
+        self._render_annotation(signode)
+        self._render_signature(signature, signode)
+        name = self._names.get(signature)
+        if name is None:
+            name = self._name_from_signature(signature)
+            # remove trailing ‘.’ found in commands, but not ‘...’ (ellipsis)
+            if name is not None and name.endswith(".") and not name.endswith("..."):
+                name = name[:-1]
+        return name
+
+    def _warn_if_duplicate_name(self, objects, name):
+        """Check that two objects in the same domain don't have the same name."""
+        if name in objects:
+            MSG = 'Duplicate object: {}; other is at {}'
+            msg = MSG.format(name, self.env.doc2path(objects[name][0]))
+            self.state_machine.reporter.warning(msg, line=self.lineno)
+
+    def _warn_if_duplicate_name(self, objects, name):
+        """Check that two objects in the same domain don't have the same name."""
+        if name in objects:
+            MSG = 'Duplicate object: {}; other is at {}'
+            msg = MSG.format(name, self.env.doc2path(objects[name][0]))
+            self.state_machine.reporter.warning(msg, line=self.lineno)
+
+    def _record_name(self, name, target_id):
+        """Record a name, mapping it to target_id
+
+        Warns if another object of the same name already exists.
+        """
+        names_in_subdomain = self.subdomain_data()
+        self._warn_if_duplicate_name(names_in_subdomain, name)
+        names_in_subdomain[name] = (self.env.docname, self.objtype, target_id)
+
+    def _target_id(self, name):
+        return make_target(self.objtype, nodes.make_id(name))
+
+    def _add_target(self, signode, name):
+        """Register a link target ‘name’, pointing to signode."""
+        targetid = self._target_id(name)
+        if targetid not in self.state.document.ids:
+            signode['ids'].append(targetid)
+            signode['names'].append(name)
+            signode['first'] = (not self.names)
+            self.state.document.note_explicit_target(signode)
+            self._record_name(name, targetid)
+        return targetid
+
+    def _add_index_entry(self, name, target):
+        """Add `name` (pointing to `target`) to the main index."""
+        assert isinstance(name, str)
+        if not name.startswith("_"):
+            # remove trailing . , found in commands, but not ... (ellipsis)
+            trim = name.endswith(".") and not name.endswith("...")
+            index_text = name[:-1] if trim else name
+            if self.index_suffix:
+                index_text += " " + self.index_suffix
+            self.indexnode['entries'].append(('single', index_text, target, '', None))
+
+    def add_target_and_index(self, name, _, signode):
+        """Attach a link target to `signode` and an index entry for `name`.
+        This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified."""
+        if name:
+            target = self._add_target(signode, name)
+            self._add_index_entry(name, target)
+            return target
+
+    def _warn_if_undocumented(self):
+        document = self.state.document
+        config = document.settings.env.config
+        report = config.report_undocumented_coq_objects
+        if report and not self.content and "undocumented" not in self.options:
+            # This is annoyingly convoluted, but we don't want to raise warnings
+            # or interrupt the generation of the current node.  For more details
+            # see https://github.com/sphinx-doc/sphinx/issues/4976.
+            msg = 'No contents in directive {}'.format(self.name)
+            node = document.reporter.info(msg, line=self.lineno)
+            getLogger(__name__).info(node.astext())
+            if report == "warning":
+                raise self.warning(msg)
+
+    def _prepare_names(self):
+        sigs = self.get_signatures()
+        names = self.options.get("name")
+        if names is None:
+            self._names = {}
+        else:
+            names = [n.strip() for n in names.split(";")]
+            if len(names) != len(sigs):
+                ERR = ("Expected {} semicolon-separated names, got {}.  " +
+                       "Please provide one name per signature line.")
+                raise self.error(ERR.format(len(names), len(sigs)))
+            self._names = dict(zip(sigs, names))
+
+    def run(self):
+        self._warn_if_undocumented()
+        self._prepare_names()
+        return super().run()
+
+class PlainObject(CoqObject):
+    """A base class for objects whose signatures should be rendered literally."""
+    def _render_signature(self, signature, signode):
+        signode += addnodes.desc_name(signature, signature)
+
+class NotationObject(CoqObject):
+    """A base class for objects whose signatures should be rendered as nested boxes.
+
+    Objects that inherit from this class can use the notation grammar (“{+ …}”,
+    “@…”, etc.) in their signature.
+    """
+    def _render_signature(self, signature, signode):
+        position = self.state_machine.get_source_and_line(self.lineno)
+        tacn_node = parse_notation(signature, *position)
+        signode += addnodes.desc_name(signature, '', tacn_node)
+
+class GallinaObject(PlainObject):
+    r"""A theorem.
+
+    Example::
+
+       .. thm:: Bound on the ceiling function
+
+          Let :math:`p` be an integer and :math:`c` a rational constant. Then
+          :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`.
+    """
+    subdomain = "thm"
+    index_suffix = "(thm)"
+    annotation = "Theorem"
+
+class VernacObject(NotationObject):
+    """A Coq command.
+
+    Example::
+
+       .. cmd:: Infix "@symbol" := @term ({+, @modifier}).
+
+          This command is equivalent to :n:`…`.
+    """
+    subdomain = "cmd"
+    index_suffix = "(cmd)"
+    annotation = "Command"
+
+    def _name_from_signature(self, signature):
+        m = re.match(r"[a-zA-Z ]+", signature)
+        if m:
+            return m.group(0).strip()
+
+class VernacVariantObject(VernacObject):
+    """A variant of a Coq command.
+
+    Example::
+
+       .. cmd:: Axiom @ident : @term.
+
+          This command links :token:`term` to the name :token:`term` as its specification in
+          the global context. The fact asserted by :token:`term` is thus assumed as a
+          postulate.
+
+          .. cmdv:: Parameter @ident : @term.
+
+             This is equivalent to :n:`Axiom @ident : @term`.
+    """
+    index_suffix = "(cmdv)"
+    annotation = "Variant"
+
+    def _name_from_signature(self, signature):
+        return None
+
+class TacticNotationObject(NotationObject):
+    """A tactic, or a tactic notation.
+
+    Example::
+
+       .. tacn:: do @num @expr
+
+          :token:`expr` is evaluated to ``v`` which must be a tactic value. …
+    """
+    subdomain = "tacn"
+    index_suffix = "(tacn)"
+    annotation = None
+
+class TacticNotationVariantObject(TacticNotationObject):
+    """A variant of a tactic.
+
+    Example::
+
+       .. tacn:: fail
+
+          This is the always-failing tactic: it does not solve any goal. It is
+          useful for defining other tacticals since it can be caught by
+          :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching
+          tacticals. …
+
+          .. tacv:: fail @natural
+
+             The number is the failure level. If no level is specified, it
+             defaults to 0. …
+    """
+    index_suffix = "(tacnv)"
+    annotation = "Variant"
+
+class OptionObject(NotationObject):
+    """A Coq option (a setting with non-boolean value, e.g. a string or numeric value).
+
+    Example::
+
+       .. opt:: Hyps Limit @num
+          :name Hyps Limit
+
+          Controls the maximum number of hypotheses displayed in goals after
+          application of a tactic.
+    """
+    subdomain = "opt"
+    index_suffix = "(opt)"
+    annotation = "Option"
+
+    def _name_from_signature(self, signature):
+        return stringify_with_ellipses(signature)
+
+
+class FlagObject(NotationObject):
+    """A Coq flag (i.e. a boolean setting).
+
+    Example::
+
+       .. flag:: Nonrecursive Elimination Schemes
+
+          Controls whether types declared with the keywords
+          :cmd:`Variant` and :cmd:`Record` get an automatic declaration of
+          induction principles.
+    """
+    subdomain = "flag"
+    index_suffix = "(flag)"
+    annotation = "Flag"
+
+    def _name_from_signature(self, signature):
+        return stringify_with_ellipses(signature)
+
+
+class TableObject(NotationObject):
+    """A Coq table, i.e. a setting that is a set of values.
+
+    Example::
+
+       .. table:: Search Blacklist @string
+          :name: Search Blacklist
+
+          Controls ...
+    """
+    subdomain = "table"
+    index_suffix = "(table)"
+    annotation = "Table"
+
+    def _name_from_signature(self, signature):
+        return stringify_with_ellipses(signature)
+
+class ProductionObject(CoqObject):
+    r"""A grammar production.
+
+    This is useful if you intend to document individual grammar productions.
+    Otherwise, use Sphinx's `production lists
+    <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
+
+    Unlike ``.. productionlist``\ s, this directive accepts notation syntax.
+
+
+    Usage::
+
+       .. prodn:: token += production
+       .. prodn:: token ::= production
+
+    Example::
+
+        .. prodn:: term += let: @pattern := @term in @term
+        .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+
+    """
+    subdomain = "prodn"
+    #annotation = "Grammar production"
+
+    def _render_signature(self, signature, signode):
+        raise NotImplementedError(self)
+
+    SIG_ERROR = ("Invalid syntax in ``.. prodn::`` directive"
+                 + "\nExpected ``name ::= ...`` or ``name += ...``"
+                 + " (e.g. ``pattern += constr:(@ident)``)")
+
+    def handle_signature(self, signature, signode):
+        nsplits = 2
+        parts = signature.split(maxsplit=nsplits)
+        if len(parts) != 3:
+            raise ExtensionError(ProductionObject.SIG_ERROR)
+
+        lhs, op, rhs = (part.strip() for part in parts)
+        if op not in ["::=", "+="]:
+            raise ExtensionError(ProductionObject.SIG_ERROR)
+
+        self._render_annotation(signode)
+
+        lhs_op = '{} {} '.format(lhs, op)
+        lhs_node = nodes.literal(lhs_op, lhs_op)
+
+        position = self.state_machine.get_source_and_line(self.lineno)
+        rhs_node = parse_notation(rhs, *position)
+        signode += addnodes.desc_name(signature, '', lhs_node, rhs_node)
+
+        return ('token', lhs) if op == '::=' else None
+
+    def _add_index_entry(self, name, target):
+        pass
+
+    def _target_id(self, name):
+        # Use `name[1]` instead of ``nodes.make_id(name[1])`` to work around
+        # https://github.com/sphinx-doc/sphinx/issues/4983
+        return 'grammar-token-{}'.format(name[1])
+
+    def _record_name(self, name, targetid):
+        env = self.state.document.settings.env
+        objects = env.domaindata['std']['objects']
+        self._warn_if_duplicate_name(objects, name)
+        objects[name] = env.docname, targetid
+
+class ExceptionObject(NotationObject):
+    """An error raised by a Coq command or tactic.
+
+    This commonly appears nested in the ``.. tacn::`` that raises the
+    exception.
+
+    Example::
+
+       .. tacv:: assert @form by @tactic
+
+          This tactic applies :n:`@tactic` to solve the subgoals generated by
+          ``assert``.
+
+          .. exn:: Proof is not complete
+
+             Raised if :n:`@tactic` does not fully solve the goal.
+    """
+    subdomain = "exn"
+    index_suffix = "(err)"
+    annotation = "Error"
+    # Uses “exn” since “err” already is a CSS class added by “writer_aux”.
+
+    # Generate names automatically
+    def _name_from_signature(self, signature):
+        return stringify_with_ellipses(signature)
+
+class WarningObject(NotationObject):
+    """An warning raised by a Coq command or tactic..
+
+    Do not mistake this for ``.. warning::``; this directive is for warning
+    messages produced by Coq.
+
+
+    Example::
+
+       .. warn:: Ambiguous path
+
+          When the coercion :token:`qualid` is added to the inheritance graph, non
+          valid coercion paths are ignored.
+    """
+    subdomain = "warn"
+    index_suffix = "(warn)"
+    annotation = "Warning"
+
+    # Generate names automatically
+    def _name_from_signature(self, signature):
+        return stringify_with_ellipses(signature)
+
+def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
+    #pylint: disable=unused-argument, dangerous-default-value
+    """Any text using the notation syntax (``@id``, ``{+, …}``, etc.).
+
+    Use this to explain tactic equivalences.  For example, you might write
+    this::
+
+       :n:`generalize @term as @ident` is just like :n:`generalize @term`, but
+       it names the introduced hypothesis :token:`ident`.
+
+    Note that this example also uses ``:token:``.  That's because ``ident`` is
+    defined in the Coq manual as a grammar production, and ``:token:``
+    creates a link to that.  When referring to a placeholder that happens to be
+    a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```.
+    """
+    notation = utils.unescape(text, 1)
+    position = inliner.reporter.get_source_and_line(lineno)
+    return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], []
+
+def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]):
+    #pylint: disable=dangerous-default-value
+    """Coq code.
+
+    Use this for Gallina and Ltac snippets::
+
+       :g:`apply plus_comm; reflexivity`
+       :g:`Set Printing All.`
+       :g:`forall (x: t), P(x)`
+    """
+    options['language'] = 'Coq'
+    return code_role(role, rawtext, text, lineno, inliner, options, content)
+    ## Too heavy:
+    ## Forked from code_role to use our custom tokenizer; this doesn't work for
+    ## snippets though: for example CoqDoc swallows the parentheses around this:
+    ## “(a: A) (b: B)”
+    # set_classes(options)
+    # classes = ['code', 'coq']
+    # code = utils.unescape(text, 1)
+    # node = nodes.literal(rawtext, '', *highlight_using_coqdoc(code), classes=classes)
+    # return [node], []
+
+CoqCodeRole = coq_code_role
+
+class CoqtopDirective(Directive):
+    r"""A reST directive to describe interactions with Coqtop.
+
+    Usage::
+
+       .. coqtop:: options…
+
+          Coq code to send to coqtop
+
+    Example::
+
+       .. coqtop:: in reset undo
+
+          Print nat.
+          Definition a := 1.
+
+    Here is a list of permissible options:
+
+    - Display options
+
+      - ``all``: Display input and output
+      - ``in``: Display only input
+      - ``out``: Display only output
+      - ``none``: Display neither (useful for setup commands)
+
+    - Behavior options
+
+      - ``reset``: Send a ``Reset Initial`` command before running this block
+      - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after
+        running all the commands in this block
+
+    ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
+    of the same document (``coqrst`` creates a single ``coqtop`` process per
+    reST source file).  Use the ``reset`` option to reset Coq's state.
+    """
+    has_content = True
+    required_arguments = 0
+    optional_arguments = 1
+    final_argument_whitespace = True
+    option_spec = { 'name': directives.unchanged }
+    directive_name = "coqtop"
+
+    def run(self):
+        # Uses a ‘container’ instead of a ‘literal_block’ to disable
+        # Pygments-based post-processing (we could also set rawsource to '')
+        content = '\n'.join(self.content)
+        args = self.arguments[0].split() if self.arguments else ['in']
+        if 'all' in args:
+            args.extend(['in', 'out'])
+        node = nodes.container(content, coqtop_options = list(set(args)),
+                               classes=['coqtop', 'literal-block'])
+        self.add_name(node)
+        return [node]
+
+class CoqdocDirective(Directive):
+    """A reST directive to display Coqtop-formatted source code.
+
+    Usage::
+
+       .. coqdoc::
+
+          Coq code to highlight
+
+    Example::
+
+       .. coqdoc::
+
+          Definition test := 1.
+    """
+    # TODO implement this as a Pygments highlighter?
+    has_content = True
+    required_arguments = 0
+    optional_arguments = 0
+    final_argument_whitespace = True
+    option_spec = { 'name': directives.unchanged }
+    directive_name = "coqdoc"
+
+    def run(self):
+        # Uses a ‘container’ instead of a ‘literal_block’ to disable
+        # Pygments-based post-processing (we could also set rawsource to '')
+        content = '\n'.join(self.content)
+        node = nodes.inline(content, '', *highlight_using_coqdoc(content))
+        wrapper = nodes.container(content, node, classes=['coqdoc', 'literal-block'])
+        self.add_name(wrapper)
+        return [wrapper]
+
+class ExampleDirective(BaseAdmonition):
+    """A reST directive for examples.
+
+    This behaves like a generic admonition; see
+    http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition
+    for more details.
+
+    Optionally, any text immediately following the ``.. example::`` header is
+    used as the example's title.
+
+    Example::
+
+       .. example:: Adding a hint to a database
+
+          The following adds ``plus_comm`` to the ``plu`` database:
+
+          .. coqdoc::
+
+             Hint Resolve plus_comm : plu.
+    """
+    node_class = nodes.admonition
+    directive_name = "example"
+    optional_arguments = 1
+
+    def run(self):
+        # ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’,
+        # and uses arguments[0] as the title in that case (in other cases, the
+        # title is unset, and it is instead set in the HTML visitor).
+        assert len(self.arguments) <= 1
+        self.arguments = [": ".join(['Example'] + self.arguments)]
+        self.options['classes'] = ['admonition', 'note']
+        return super().run()
+
+class PreambleDirective(Directive):
+    r"""A reST directive to include a TeX file.
+
+    Mostly useful to let MathJax know about `\def`s and `\newcommand`s.  The
+    contents of the TeX file are wrapped in a math environment, as MathJax
+    doesn't process LaTeX definitions otherwise.
+
+    Usage::
+
+       .. preamble:: preamble.tex
+    """
+    has_content = False
+    required_arguments = 1
+    optional_arguments = 0
+    final_argument_whitespace = True
+    option_spec = {}
+    directive_name = "preamble"
+
+    def run(self):
+        document = self.state.document
+        env = document.settings.env
+
+        if not document.settings.file_insertion_enabled:
+            msg = 'File insertion disabled'
+            return [document.reporter.warning(msg, line=self.lineno)]
+
+        rel_fname, abs_fname = env.relfn2path(self.arguments[0])
+        env.note_dependency(rel_fname)
+
+        with open(abs_fname, encoding="utf-8") as ltx:
+            latex = ltx.read()
+
+        node = make_math_node(latex, env.docname, nowrap=False)
+        node['classes'] = ["math-preamble"]
+        set_source_info(self, node)
+        return [node]
+
+class InferenceDirective(Directive):
+    r"""A reST directive to format inference rules.
+
+    This also serves as a small illustration of the way to create new Sphinx
+    directives.
+
+    Usage::
+
+       .. inference:: name
+
+          newline-separated premises
+          --------------------------
+          conclusion
+
+    Example::
+
+       .. inference:: Prod-Pro
+
+          \WTEG{T}{s}
+          s \in \Sort
+          \WTE{\Gamma::(x:T)}{U}{\Prop}
+          -----------------------------
+          \WTEG{\forall~x:T,U}{\Prop}
+    """
+    required_arguments = 1
+    optional_arguments = 0
+    has_content = True
+    final_argument_whitespace = True
+    directive_name = "inference"
+
+    @staticmethod
+    def prepare_latex_operand(op):
+        # TODO: Could use a fancier inference class in LaTeX
+        return '%\n\\hspace{3em}%\n'.join(op.strip().splitlines())
+
+    def prepare_latex(self, content):
+        parts = re.split('^ *----+ *$', content, flags=re.MULTILINE)
+        if len(parts) != 2:
+            raise self.error('Expected two parts in ‘inference’ directive, separated by a rule (----).')
+
+        top, bottom = tuple(InferenceDirective.prepare_latex_operand(p) for p in parts)
+        return "%\n".join(("\\frac{", top, "}{", bottom, "}"))
+
+    def run(self):
+        self.assert_has_content()
+
+        title = self.arguments[0]
+        content = '\n'.join(self.content)
+        latex = self.prepare_latex(content)
+        docname = self.state.document.settings.env.docname
+        math_node = make_math_node(latex, docname, nowrap=False)
+
+        tid = nodes.make_id(title)
+        target = nodes.target('', '', ids=['inference-' + tid])
+        self.state.document.note_explicit_target(target)
+
+        term, desc = nodes.term('', title), nodes.description('', math_node)
+        dli = nodes.definition_list_item('', term, desc)
+        dl = nodes.definition_list(content, target, dli)
+        set_source_info(self, dl)
+        return [dl]
+
+class AnsiColorsParser():
+    """Parse ANSI-colored output from Coqtop into Sphinx nodes."""
+
+    # Coqtop's output crashes ansi.py, because it contains a bunch of extended codes
+    # This class is a fork of the original ansi.py, released under a BSD license in sphinx-contribs
+
+    COLOR_PATTERN = re.compile('\x1b\\[([^m]+)m')
+
+    def __init__(self):
+        self.new_nodes, self.pending_nodes = [], []
+
+    def _finalize_pending_nodes(self):
+        self.new_nodes.extend(self.pending_nodes)
+        self.pending_nodes = []
+
+    def _add_text(self, raw, beg, end):
+        if beg < end:
+            text = raw[beg:end]
+            if self.pending_nodes:
+                self.pending_nodes[-1].append(nodes.Text(text))
+            else:
+                self.new_nodes.append(nodes.inline('', text))
+
+    def colorize_str(self, raw):
+        """Parse raw (an ANSI-colored output string from Coqtop) into Sphinx nodes."""
+        last_end = 0
+        for match in AnsiColorsParser.COLOR_PATTERN.finditer(raw):
+            self._add_text(raw, last_end, match.start())
+            last_end = match.end()
+            classes = ansicolors.parse_ansi(match.group(1))
+            if 'ansi-reset' in classes:
+                self._finalize_pending_nodes()
+            else:
+                node = nodes.inline()
+                self.pending_nodes.append(node)
+                node['classes'].extend(classes)
+        self._add_text(raw, last_end, len(raw))
+        self._finalize_pending_nodes()
+        return self.new_nodes
+
+class CoqtopBlocksTransform(Transform):
+    """Filter handling the actual work for the coqtop directive
+
+    Adds coqtop's responses, colorizes input and output, and merges consecutive
+    coqtop directives for better visual rendition.
+    """
+    default_priority = 10
+
+    @staticmethod
+    def is_coqtop_block(node):
+        return isinstance(node, nodes.Element) and 'coqtop_options' in node
+
+    @staticmethod
+    def split_sentences(source):
+        """Split Coq sentences in source. Could be improved."""
+        return re.split(r"(?<=(?<!\.)\.)\s+", source)
+
+    @staticmethod
+    def parse_options(options):
+        """Parse options according to the description in CoqtopDirective."""
+        opt_undo = 'undo' in options
+        opt_reset = 'reset' in options
+        opt_all, opt_none = 'all' in options, 'none' in options
+        opt_input, opt_output = opt_all or 'in' in options, opt_all or 'out' in options
+
+        unexpected_options = list(set(options) - set(('reset', 'undo', 'all', 'none', 'in', 'out')))
+        if unexpected_options:
+            raise ValueError("Unexpected options for .. coqtop:: {}".format(unexpected_options))
+        elif (opt_input or opt_output) and opt_none:
+            raise ValueError("Inconsistent options for .. coqtop:: ‘none’ with ‘in’, ‘out’, or ‘all’")
+        elif opt_reset and opt_undo:
+            raise ValueError("Inconsistent options for .. coqtop:: ‘undo’ with ‘reset’")
+
+        return opt_undo, opt_reset, opt_input and not opt_none, opt_output and not opt_none
+
+    @staticmethod
+    def block_classes(should_show, contents=None):
+        """Compute classes to add to a node containing contents.
+
+        :param should_show: Whether this node should be displayed"""
+        is_empty = contents is not None and re.match(r"^\s*$", contents)
+        if is_empty or not should_show:
+            return ['coqtop-hidden']
+        else:
+            return []
+
+    @staticmethod
+    def make_rawsource(pairs, opt_input, opt_output):
+        blocks = []
+        for sentence, output in pairs:
+            output = AnsiColorsParser.COLOR_PATTERN.sub("", output).strip()
+            if opt_input:
+                blocks.append(sentence)
+            if output and opt_output:
+                blocks.append(re.sub("^", "    ", output, flags=re.MULTILINE) + "\n")
+        return '\n'.join(blocks)
+
+    def add_coqtop_output(self):
+        """Add coqtop's responses to a Sphinx AST
+
+        Finds nodes to process using is_coqtop_block."""
+        with CoqTop(color=True) as repl:
+            for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block):
+                options = node['coqtop_options']
+                opt_undo, opt_reset, opt_input, opt_output = self.parse_options(options)
+
+                if opt_reset:
+                    repl.sendone("Reset Initial.")
+                pairs = []
+                for sentence in self.split_sentences(node.rawsource):
+                    pairs.append((sentence, repl.sendone(sentence)))
+                if opt_undo:
+                    repl.sendone("Undo {}.".format(len(pairs)))
+
+                dli = nodes.definition_list_item()
+                for sentence, output in pairs:
+                    # Use Coqdoq to highlight input
+                    in_chunks = highlight_using_coqdoc(sentence)
+                    dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input))
+                    # Parse ANSI sequences to highlight output
+                    out_chunks = AnsiColorsParser().colorize_str(output)
+                    dli += nodes.definition(output, *out_chunks, classes=self.block_classes(opt_output, output))
+                node.clear()
+                node.rawsource = self.make_rawsource(pairs, opt_input, opt_output)
+                node['classes'].extend(self.block_classes(opt_input or opt_output))
+                node += nodes.inline('', '', classes=['coqtop-reset'] * opt_reset)
+                node += nodes.definition_list(node.rawsource, dli)
+
+    @staticmethod
+    def merge_coqtop_classes(kept_node, discarded_node):
+        discarded_classes = discarded_node['classes']
+        if not 'coqtop-hidden' in discarded_classes:
+            kept_node['classes'] = [c for c in kept_node['classes']
+                                    if c != 'coqtop-hidden']
+
+    @staticmethod
+    def merge_consecutive_coqtop_blocks(app, doctree, _):
+        """Merge consecutive divs wrapping lists of Coq sentences; keep ‘dl’s separate."""
+        for node in doctree.traverse(CoqtopBlocksTransform.is_coqtop_block):
+            if node.parent:
+                rawsources, names = [node.rawsource], set(node['names'])
+                for sibling in node.traverse(include_self=False, descend=False,
+                                             siblings=True, ascend=False):
+                    if CoqtopBlocksTransform.is_coqtop_block(sibling):
+                        CoqtopBlocksTransform.merge_coqtop_classes(node, sibling)
+                        rawsources.append(sibling.rawsource)
+                        names.update(sibling['names'])
+                        node.extend(sibling.children)
+                        node.parent.remove(sibling)
+                        sibling.parent = None
+                    else:
+                        break
+                node.rawsource = "\n\n".join(rawsources)
+                node['names'] = list(names)
+
+    def apply(self):
+        self.add_coqtop_output()
+
+class CoqSubdomainsIndex(Index):
+    """Index subclass to provide subdomain-specific indices.
+
+    Just as in the original manual, we want to have separate indices for each
+    Coq subdomain (tactics, commands, options, etc)"""
+
+    name, localname, shortname, subdomains = None, None, None, [] # Must be overwritten
+
+    def generate(self, docnames=None):
+        content = defaultdict(list)
+        items = chain(*(self.domain.data['objects'][subdomain].items()
+                        for subdomain in self.subdomains))
+
+        for itemname, (docname, _, anchor) in sorted(items, key=lambda x: x[0].lower()):
+            if docnames and docname not in docnames:
+                continue
+
+            entries = content[itemname[0].lower()]
+            entries.append([itemname, 0, docname, anchor, '', '', ''])
+
+        collapse = False
+        content = sorted(content.items())
+        return content, collapse
+
+class CoqVernacIndex(CoqSubdomainsIndex):
+    name, localname, shortname, subdomains = "cmdindex", "Command Index", "commands", ["cmd"]
+
+class CoqTacticIndex(CoqSubdomainsIndex):
+    name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tacn"]
+
+class CoqOptionIndex(CoqSubdomainsIndex):
+    name, localname, shortname, subdomains = "optindex", "Flags, options and Tables Index", "options", ["flag", "opt", "table"]
+
+class CoqGallinaIndex(CoqSubdomainsIndex):
+    name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"]
+
+class CoqExceptionIndex(CoqSubdomainsIndex):
+    name, localname, shortname, subdomains = "exnindex", "Errors and Warnings Index", "errors", ["exn", "warn"]
+
+class IndexXRefRole(XRefRole):
+    """A link to one of our domain-specific indices."""
+    lowercase = True,
+    innernodeclass = nodes.inline
+    warn_dangling = True
+
+    def process_link(self, env, refnode, has_explicit_title, title, target):
+        if not has_explicit_title:
+            index = CoqDomain.find_index_by_name(target)
+            if index:
+                title = index.localname
+        return title, target
+
+def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
+    """A grammar production not included in a ``productionlist`` directive.
+
+    Useful to informally introduce a production, as part of running text.
+
+    Example::
+
+       :production:`string` indicates a quoted string.
+
+    You're not likely to use this role very commonly; instead, use a
+    `production list
+    <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_
+    and reference its tokens using ``:token:`…```.
+    """
+    #pylint: disable=dangerous-default-value, unused-argument
+    env = inliner.document.settings.env
+    targetid = 'grammar-token-{}'.format(text)
+    target = nodes.target('', '', ids=[targetid])
+    inliner.document.note_explicit_target(target)
+    code = nodes.literal(rawtext, text, role=typ.lower())
+    node = nodes.inline(rawtext, '', target, code, classes=['inline-grammar-production'])
+    set_role_source_info(inliner, lineno, node)
+    env.domaindata['std']['objects']['token', text] = env.docname, targetid
+    return [node], []
+
+GrammarProductionRole.role_name = "production"
+
+class CoqDomain(Domain):
+    """A domain to document Coq code.
+
+    Sphinx has a notion of “domains”, used to tailor it to a specific language.
+    Domains mostly consist in descriptions of the objects that we wish to
+    describe (for Coq, this includes tactics, tactic notations, options,
+    exceptions, etc.), as well as domain-specific roles and directives.
+
+    Each domain is responsible for tracking its objects, and resolving
+    references to them. In the case of Coq, this leads us to define Coq
+    “subdomains”, which classify objects into categories in which names must be
+    unique. For example, a tactic and a theorem may share a name, but two
+    tactics cannot be named the same.
+    """
+
+    name = 'coq'
+    label = 'Coq'
+
+    object_types = {
+        # ObjType (= directive type) → (Local name, *xref-roles)
+        'cmd': ObjType('cmd', 'cmd'),
+        'cmdv': ObjType('cmdv', 'cmd'),
+        'tacn': ObjType('tacn', 'tacn'),
+        'tacv': ObjType('tacv', 'tacn'),
+        'opt': ObjType('opt', 'opt'),
+        'flag': ObjType('flag', 'flag'),
+        'table': ObjType('table', 'table'),
+        'thm': ObjType('thm', 'thm'),
+        'prodn': ObjType('prodn', 'prodn'),
+        'exn': ObjType('exn', 'exn'),
+        'warn': ObjType('warn', 'exn'),
+        'index': ObjType('index', 'index', searchprio=-1)
+    }
+
+    directives = {
+        # Note that some directives live in the same semantic subdomain; ie
+        # there's one directive per object type, but some object types map to
+        # the same role.
+        'cmd': VernacObject,
+        'cmdv': VernacVariantObject,
+        'tacn': TacticNotationObject,
+        'tacv': TacticNotationVariantObject,
+        'opt': OptionObject,
+        'flag': FlagObject,
+        'table': TableObject,
+        'thm': GallinaObject,
+        'prodn' : ProductionObject,
+        'exn': ExceptionObject,
+        'warn': WarningObject,
+    }
+
+    roles = {
+        # Each of these roles lives in a different semantic “subdomain”
+        'cmd': XRefRole(warn_dangling=True),
+        'tacn': XRefRole(warn_dangling=True),
+        'opt': XRefRole(warn_dangling=True),
+        'flag': XRefRole(warn_dangling=True),
+        'table': XRefRole(warn_dangling=True),
+        'thm': XRefRole(warn_dangling=True),
+        'prodn' : XRefRole(warn_dangling=True),
+        'exn': XRefRole(warn_dangling=True),
+        'warn': XRefRole(warn_dangling=True),
+        # This one is special
+        'index': IndexXRefRole(),
+        # These are used for highlighting
+        'n': NotationRole,
+        'g': CoqCodeRole
+    }
+
+    indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqExceptionIndex]
+
+    data_version = 1
+    initial_data = {
+        # Collect everything under a key that we control, since Sphinx adds
+        # others, such as “version”
+        'objects' : { # subdomain → name → docname, objtype, targetid
+            'cmd': {},
+            'tacn': {},
+            'opt': {},
+            'flag': {},
+            'table': {},
+            'thm': {},
+            'prodn' : {},
+            'exn': {},
+            'warn': {},
+        }
+    }
+
+    @staticmethod
+    def find_index_by_name(targetid):
+        for index in CoqDomain.indices:
+            if index.name == targetid:
+                return index
+
+    def get_objects(self):
+        # Used for searching and object inventories (intersphinx)
+        for _, objects in self.data['objects'].items():
+            for name, (docname, objtype, targetid) in objects.items():
+                yield (name, name, objtype, docname, targetid, self.object_types[objtype].attrs['searchprio'])
+        for index in self.indices:
+            yield (index.name, index.localname, 'index', "coq-" + index.name, '', -1)
+
+    def merge_domaindata(self, docnames, otherdata):
+        DUP = "Duplicate declaration: '{}' also defined in '{}'.\n"
+        for subdomain, their_objects in otherdata['objects'].items():
+            our_objects = self.data['objects'][subdomain]
+            for name, (docname, objtype, targetid) in their_objects.items():
+                if docname in docnames:
+                    if name in our_objects:
+                        self.env.warn(docname, DUP.format(name, our_objects[name][0]))
+                    our_objects[name] = (docname, objtype, targetid)
+
+    def resolve_xref(self, env, fromdocname, builder, role, targetname, node, contnode):
+        # ‘target’ is the name that was written in the document
+        # ‘role’ is where this xref comes from; it's exactly one of our subdomains
+        if role == 'index':
+            index = CoqDomain.find_index_by_name(targetname)
+            if index:
+                return make_refnode(builder, fromdocname, "coq-" + index.name, '', contnode, index.localname)
+        else:
+            resolved = self.data['objects'][role].get(targetname)
+            if resolved:
+                (todocname, _, targetid) = resolved
+                return make_refnode(builder, fromdocname, todocname, targetid, contnode, targetname)
+
+    def clear_doc(self, docname_to_clear):
+        for subdomain_objects in self.data['objects'].values():
+            for name, (docname, _, _) in list(subdomain_objects.items()):
+                if docname == docname_to_clear:
+                    del subdomain_objects[name]
+
+def is_coqtop_or_coqdoc_block(node):
+    return (isinstance(node, nodes.Element) and
+       ('coqtop' in node['classes'] or 'coqdoc' in node['classes']))
+
+def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint: disable=unused-argument
+    """Simplify coqdoc and coqtop blocks.
+
+    In HTML mode, this does nothing; in other formats, such as LaTeX, it
+    replaces coqdoc and coqtop blocks by plain text sources, which will use
+    pygments if available.  This prevents the LaTeX builder from getting
+    confused.
+    """
+    is_html = app.builder.tags.has("html")
+    for node in doctree.traverse(is_coqtop_or_coqdoc_block):
+        if is_html:
+            node.rawsource = '' # Prevent pygments from kicking in
+        elif 'coqtop-hidden' in node['classes']:
+            node.parent.remove(node)
+        else:
+            node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq"))
+
+COQ_ADDITIONAL_DIRECTIVES = [CoqtopDirective,
+                             CoqdocDirective,
+                             ExampleDirective,
+                             InferenceDirective,
+                             PreambleDirective]
+
+COQ_ADDITIONAL_ROLES = [GrammarProductionRole]
+
+def setup(app):
+    """Register the Coq domain"""
+
+    # A few sanity checks:
+    subdomains = set(obj.subdomain for obj in CoqDomain.directives.values())
+    assert subdomains.issuperset(chain(*(idx.subdomains for idx in CoqDomain.indices)))
+    assert subdomains.issubset(CoqDomain.roles.keys())
+
+    # Add domain, directives, and roles
+    app.add_domain(CoqDomain)
+
+    for role in COQ_ADDITIONAL_ROLES:
+        app.add_role(role.role_name, role)
+
+    for directive in COQ_ADDITIONAL_DIRECTIVES:
+        app.add_directive(directive.directive_name, directive)
+
+    app.add_transform(CoqtopBlocksTransform)
+    app.connect('doctree-resolved', simplify_source_code_blocks_for_latex)
+    app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks)
+
+    # Add extra styles
+    app.add_stylesheet("fonts.css")
+    app.add_stylesheet("ansi.css")
+    app.add_stylesheet("coqdoc.css")
+    app.add_javascript("notations.js")
+    app.add_stylesheet("notations.css")
+    app.add_stylesheet("pre-text.css")
+
+    # Tell Sphinx about extra settings
+    app.add_config_value("report_undocumented_coq_objects", None, 'env')
+
+    # ``env_version`` is used by Sphinx to know when to invalidate
+    # coqdomain-specific bits in its caches.  It should be incremented when the
+    # contents of ``env.domaindata['coq']`` change.  See
+    # `https://github.com/sphinx-doc/sphinx/issues/4460`.
+    meta = { "version": "0.1",
+             "env_version": 2,
+             "parallel_read_safe": True }
+    return meta
diff --git a/doc/tools/coqrst/notations/Makefile b/doc/tools/coqrst/notations/Makefile
new file mode 100644
index 00000000..c017aed9
--- /dev/null
+++ b/doc/tools/coqrst/notations/Makefile
@@ -0,0 +1,27 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+# Parsing compact tactic notation syntax in
+
+TEST_INPUT="unfold {+, @qualid|@string at {+, num}}"
+
+python:
+	antlr4 -Dlanguage=Python3 -visitor -no-listener TacticNotations.g
+
+java:
+	antlr4 -Dlanguage=Java TacticNotations.g && javac TacticNotations*.java
+
+test: java
+	grun TacticNotations top -tree <<< "$(TEST_INPUT)"
+
+gui: java
+	grun TacticNotations top -gui <<< "$(TEST_INPUT)"
+
+sample:
+	cd ..; python3 -m coqnotations.driver < ../tests/tactics > ../tests/antlr-notations.html
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g
new file mode 100644
index 00000000..a889ebda
--- /dev/null
+++ b/doc/tools/coqrst/notations/TacticNotations.g
@@ -0,0 +1,33 @@
+/************************************************************************/
+/*         *   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)         */
+/************************************************************************/
+grammar TacticNotations;
+
+// Terminals are not visited, so we add non-terminals for each terminal that
+// needs rendering (in particular whitespace (kept in output) vs. WHITESPACE
+// (discarded)).
+
+top: blocks EOF;
+blocks: block ((whitespace)? block)*;
+block: atomic | meta | hole | repeat | curlies;
+repeat: LGROUP (ATOM)? WHITESPACE blocks (WHITESPACE)? RBRACE;
+curlies: LBRACE (whitespace)? blocks (whitespace)? RBRACE;
+whitespace: WHITESPACE;
+meta: METACHAR;
+atomic: ATOM (SUB)?;
+hole: ID (SUB)?;
+
+LGROUP: '{' [+*?];
+LBRACE: '{';
+RBRACE: '}';
+METACHAR: '%' [|(){}];
+ATOM: '@' | '_' | ~[@_{} ]+;
+ID: '@' ('_'? [a-zA-Z0-9])+;
+SUB: '_' '_' [a-zA-Z0-9]+;
+WHITESPACE: ' '+;
diff --git a/doc/tools/coqrst/notations/TacticNotations.tokens b/doc/tools/coqrst/notations/TacticNotations.tokens
new file mode 100644
index 00000000..88b38f97
--- /dev/null
+++ b/doc/tools/coqrst/notations/TacticNotations.tokens
@@ -0,0 +1,10 @@
+LGROUP=1
+LBRACE=2
+RBRACE=3
+METACHAR=4
+ATOM=5
+ID=6
+SUB=7
+WHITESPACE=8
+'{'=2
+'}'=3
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py
new file mode 100644
index 00000000..27293e7e
--- /dev/null
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py
@@ -0,0 +1,71 @@
+# Generated from TacticNotations.g by ANTLR 4.7
+from antlr4 import *
+from io import StringIO
+from typing.io import TextIO
+import sys
+
+
+def serializedATN():
+    with StringIO() as buf:
+        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\n")
+        buf.write(":\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7")
+        buf.write("\4\b\t\b\4\t\t\t\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3")
+        buf.write("\5\3\6\3\6\6\6 \n\6\r\6\16\6!\5\6$\n\6\3\7\3\7\5\7(\n")
+        buf.write("\7\3\7\6\7+\n\7\r\7\16\7,\3\b\3\b\3\b\6\b\62\n\b\r\b\16")
+        buf.write("\b\63\3\t\6\t\67\n\t\r\t\16\t8\2\2\n\3\3\5\4\7\5\t\6\13")
+        buf.write("\7\r\b\17\t\21\n\3\2\7\4\2,-AA\4\2*+}\177\4\2BBaa\7\2")
+        buf.write("\"\"BBaa}}\177\177\5\2\62;C\\c|\2?\2\3\3\2\2\2\2\5\3\2")
+        buf.write("\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2")
+        buf.write("\2\17\3\2\2\2\2\21\3\2\2\2\3\23\3\2\2\2\5\26\3\2\2\2\7")
+        buf.write("\30\3\2\2\2\t\32\3\2\2\2\13#\3\2\2\2\r%\3\2\2\2\17.\3")
+        buf.write("\2\2\2\21\66\3\2\2\2\23\24\7}\2\2\24\25\t\2\2\2\25\4\3")
+        buf.write("\2\2\2\26\27\7}\2\2\27\6\3\2\2\2\30\31\7\177\2\2\31\b")
+        buf.write("\3\2\2\2\32\33\7\'\2\2\33\34\t\3\2\2\34\n\3\2\2\2\35$")
+        buf.write("\t\4\2\2\36 \n\5\2\2\37\36\3\2\2\2 !\3\2\2\2!\37\3\2\2")
+        buf.write("\2!\"\3\2\2\2\"$\3\2\2\2#\35\3\2\2\2#\37\3\2\2\2$\f\3")
+        buf.write("\2\2\2%*\7B\2\2&(\7a\2\2\'&\3\2\2\2\'(\3\2\2\2()\3\2\2")
+        buf.write("\2)+\t\6\2\2*\'\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2")
+        buf.write("-\16\3\2\2\2./\7a\2\2/\61\7a\2\2\60\62\t\6\2\2\61\60\3")
+        buf.write("\2\2\2\62\63\3\2\2\2\63\61\3\2\2\2\63\64\3\2\2\2\64\20")
+        buf.write("\3\2\2\2\65\67\7\"\2\2\66\65\3\2\2\2\678\3\2\2\28\66\3")
+        buf.write("\2\2\289\3\2\2\29\22\3\2\2\2\t\2!#\',\638\2")
+        return buf.getvalue()
+
+
+class TacticNotationsLexer(Lexer):
+
+    atn = ATNDeserializer().deserialize(serializedATN())
+
+    decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ]
+
+    LGROUP = 1
+    LBRACE = 2
+    RBRACE = 3
+    METACHAR = 4
+    ATOM = 5
+    ID = 6
+    SUB = 7
+    WHITESPACE = 8
+
+    channelNames = [ u"DEFAULT_TOKEN_CHANNEL", u"HIDDEN" ]
+
+    modeNames = [ "DEFAULT_MODE" ]
+
+    literalNames = [ "<INVALID>",
+            "'{'", "'}'" ]
+
+    symbolicNames = [ "<INVALID>",
+            "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID", "SUB",
+            "WHITESPACE" ]
+
+    ruleNames = [ "LGROUP", "LBRACE", "RBRACE", "METACHAR", "ATOM", "ID",
+                  "SUB", "WHITESPACE" ]
+
+    grammarFileName = "TacticNotations.g"
+
+    def __init__(self, input=None, output:TextIO = sys.stdout):
+        super().__init__(input, output)
+        self.checkVersion("4.7")
+        self._interp = LexerATNSimulator(self, self.atn, self.decisionsToDFA, PredictionContextCache())
+        self._actions = None
+        self._predicates = None
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.tokens b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
new file mode 100644
index 00000000..88b38f97
--- /dev/null
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.tokens
@@ -0,0 +1,10 @@
+LGROUP=1
+LBRACE=2
+RBRACE=3
+METACHAR=4
+ATOM=5
+ID=6
+SUB=7
+WHITESPACE=8
+'{'=2
+'}'=3
diff --git a/doc/tools/coqrst/notations/TacticNotationsParser.py b/doc/tools/coqrst/notations/TacticNotationsParser.py
new file mode 100644
index 00000000..645f0789
--- /dev/null
+++ b/doc/tools/coqrst/notations/TacticNotationsParser.py
@@ -0,0 +1,595 @@
+# Generated from TacticNotations.g by ANTLR 4.7
+# encoding: utf-8
+from antlr4 import *
+from io import StringIO
+from typing.io import TextIO
+import sys
+
+def serializedATN():
+    with StringIO() as buf:
+        buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\3\n")
+        buf.write("J\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7\4\b")
+        buf.write("\t\b\4\t\t\t\4\n\t\n\3\2\3\2\3\2\3\3\3\3\5\3\32\n\3\3")
+        buf.write("\3\7\3\35\n\3\f\3\16\3 \13\3\3\4\3\4\3\4\3\4\3\4\5\4\'")
+        buf.write("\n\4\3\5\3\5\5\5+\n\5\3\5\3\5\3\5\5\5\60\n\5\3\5\3\5\3")
+        buf.write("\6\3\6\5\6\66\n\6\3\6\3\6\5\6:\n\6\3\6\3\6\3\7\3\7\3\b")
+        buf.write("\3\b\3\t\3\t\5\tD\n\t\3\n\3\n\5\nH\n\n\3\n\2\2\13\2\4")
+        buf.write("\6\b\n\f\16\20\22\2\2\2L\2\24\3\2\2\2\4\27\3\2\2\2\6&")
+        buf.write("\3\2\2\2\b(\3\2\2\2\n\63\3\2\2\2\f=\3\2\2\2\16?\3\2\2")
+        buf.write("\2\20A\3\2\2\2\22E\3\2\2\2\24\25\5\4\3\2\25\26\7\2\2\3")
+        buf.write("\26\3\3\2\2\2\27\36\5\6\4\2\30\32\5\f\7\2\31\30\3\2\2")
+        buf.write("\2\31\32\3\2\2\2\32\33\3\2\2\2\33\35\5\6\4\2\34\31\3\2")
+        buf.write("\2\2\35 \3\2\2\2\36\34\3\2\2\2\36\37\3\2\2\2\37\5\3\2")
+        buf.write("\2\2 \36\3\2\2\2!\'\5\20\t\2\"\'\5\16\b\2#\'\5\22\n\2")
+        buf.write("$\'\5\b\5\2%\'\5\n\6\2&!\3\2\2\2&\"\3\2\2\2&#\3\2\2\2")
+        buf.write("&$\3\2\2\2&%\3\2\2\2\'\7\3\2\2\2(*\7\3\2\2)+\7\7\2\2*")
+        buf.write(")\3\2\2\2*+\3\2\2\2+,\3\2\2\2,-\7\n\2\2-/\5\4\3\2.\60")
+        buf.write("\7\n\2\2/.\3\2\2\2/\60\3\2\2\2\60\61\3\2\2\2\61\62\7\5")
+        buf.write("\2\2\62\t\3\2\2\2\63\65\7\4\2\2\64\66\5\f\7\2\65\64\3")
+        buf.write("\2\2\2\65\66\3\2\2\2\66\67\3\2\2\2\679\5\4\3\28:\5\f\7")
+        buf.write("\298\3\2\2\29:\3\2\2\2:;\3\2\2\2;<\7\5\2\2<\13\3\2\2\2")
+        buf.write("=>\7\n\2\2>\r\3\2\2\2?@\7\6\2\2@\17\3\2\2\2AC\7\7\2\2")
+        buf.write("BD\7\t\2\2CB\3\2\2\2CD\3\2\2\2D\21\3\2\2\2EG\7\b\2\2F")
+        buf.write("H\7\t\2\2GF\3\2\2\2GH\3\2\2\2H\23\3\2\2\2\13\31\36&*/")
+        buf.write("\659CG")
+        return buf.getvalue()
+
+
+class TacticNotationsParser ( Parser ):
+
+    grammarFileName = "TacticNotations.g"
+
+    atn = ATNDeserializer().deserialize(serializedATN())
+
+    decisionsToDFA = [ DFA(ds, i) for i, ds in enumerate(atn.decisionToState) ]
+
+    sharedContextCache = PredictionContextCache()
+
+    literalNames = [ "<INVALID>", "<INVALID>", "'{'", "'}'" ]
+
+    symbolicNames = [ "<INVALID>", "LGROUP", "LBRACE", "RBRACE", "METACHAR",
+                      "ATOM", "ID", "SUB", "WHITESPACE" ]
+
+    RULE_top = 0
+    RULE_blocks = 1
+    RULE_block = 2
+    RULE_repeat = 3
+    RULE_curlies = 4
+    RULE_whitespace = 5
+    RULE_meta = 6
+    RULE_atomic = 7
+    RULE_hole = 8
+
+    ruleNames =  [ "top", "blocks", "block", "repeat", "curlies", "whitespace",
+                   "meta", "atomic", "hole" ]
+
+    EOF = Token.EOF
+    LGROUP=1
+    LBRACE=2
+    RBRACE=3
+    METACHAR=4
+    ATOM=5
+    ID=6
+    SUB=7
+    WHITESPACE=8
+
+    def __init__(self, input:TokenStream, output:TextIO = sys.stdout):
+        super().__init__(input, output)
+        self.checkVersion("4.7")
+        self._interp = ParserATNSimulator(self, self.atn, self.decisionsToDFA, self.sharedContextCache)
+        self._predicates = None
+
+
+
+    class TopContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def blocks(self):
+            return self.getTypedRuleContext(TacticNotationsParser.BlocksContext,0)
+
+
+        def EOF(self):
+            return self.getToken(TacticNotationsParser.EOF, 0)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_top
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitTop" ):
+                return visitor.visitTop(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def top(self):
+
+        localctx = TacticNotationsParser.TopContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 0, self.RULE_top)
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 18
+            self.blocks()
+            self.state = 19
+            self.match(TacticNotationsParser.EOF)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class BlocksContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def block(self, i:int=None):
+            if i is None:
+                return self.getTypedRuleContexts(TacticNotationsParser.BlockContext)
+            else:
+                return self.getTypedRuleContext(TacticNotationsParser.BlockContext,i)
+
+
+        def whitespace(self, i:int=None):
+            if i is None:
+                return self.getTypedRuleContexts(TacticNotationsParser.WhitespaceContext)
+            else:
+                return self.getTypedRuleContext(TacticNotationsParser.WhitespaceContext,i)
+
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_blocks
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitBlocks" ):
+                return visitor.visitBlocks(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def blocks(self):
+
+        localctx = TacticNotationsParser.BlocksContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 2, self.RULE_blocks)
+        self._la = 0 # Token type
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 21
+            self.block()
+            self.state = 28
+            self._errHandler.sync(self)
+            _alt = self._interp.adaptivePredict(self._input,1,self._ctx)
+            while _alt!=2 and _alt!=ATN.INVALID_ALT_NUMBER:
+                if _alt==1:
+                    self.state = 23
+                    self._errHandler.sync(self)
+                    _la = self._input.LA(1)
+                    if _la==TacticNotationsParser.WHITESPACE:
+                        self.state = 22
+                        self.whitespace()
+
+
+                    self.state = 25
+                    self.block()
+                self.state = 30
+                self._errHandler.sync(self)
+                _alt = self._interp.adaptivePredict(self._input,1,self._ctx)
+
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class BlockContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def atomic(self):
+            return self.getTypedRuleContext(TacticNotationsParser.AtomicContext,0)
+
+
+        def meta(self):
+            return self.getTypedRuleContext(TacticNotationsParser.MetaContext,0)
+
+
+        def hole(self):
+            return self.getTypedRuleContext(TacticNotationsParser.HoleContext,0)
+
+
+        def repeat(self):
+            return self.getTypedRuleContext(TacticNotationsParser.RepeatContext,0)
+
+
+        def curlies(self):
+            return self.getTypedRuleContext(TacticNotationsParser.CurliesContext,0)
+
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_block
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitBlock" ):
+                return visitor.visitBlock(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def block(self):
+
+        localctx = TacticNotationsParser.BlockContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 4, self.RULE_block)
+        try:
+            self.state = 36
+            self._errHandler.sync(self)
+            token = self._input.LA(1)
+            if token in [TacticNotationsParser.ATOM]:
+                self.enterOuterAlt(localctx, 1)
+                self.state = 31
+                self.atomic()
+                pass
+            elif token in [TacticNotationsParser.METACHAR]:
+                self.enterOuterAlt(localctx, 2)
+                self.state = 32
+                self.meta()
+                pass
+            elif token in [TacticNotationsParser.ID]:
+                self.enterOuterAlt(localctx, 3)
+                self.state = 33
+                self.hole()
+                pass
+            elif token in [TacticNotationsParser.LGROUP]:
+                self.enterOuterAlt(localctx, 4)
+                self.state = 34
+                self.repeat()
+                pass
+            elif token in [TacticNotationsParser.LBRACE]:
+                self.enterOuterAlt(localctx, 5)
+                self.state = 35
+                self.curlies()
+                pass
+            else:
+                raise NoViableAltException(self)
+
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class RepeatContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def LGROUP(self):
+            return self.getToken(TacticNotationsParser.LGROUP, 0)
+
+        def WHITESPACE(self, i:int=None):
+            if i is None:
+                return self.getTokens(TacticNotationsParser.WHITESPACE)
+            else:
+                return self.getToken(TacticNotationsParser.WHITESPACE, i)
+
+        def blocks(self):
+            return self.getTypedRuleContext(TacticNotationsParser.BlocksContext,0)
+
+
+        def RBRACE(self):
+            return self.getToken(TacticNotationsParser.RBRACE, 0)
+
+        def ATOM(self):
+            return self.getToken(TacticNotationsParser.ATOM, 0)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_repeat
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitRepeat" ):
+                return visitor.visitRepeat(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def repeat(self):
+
+        localctx = TacticNotationsParser.RepeatContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 6, self.RULE_repeat)
+        self._la = 0 # Token type
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 38
+            self.match(TacticNotationsParser.LGROUP)
+            self.state = 40
+            self._errHandler.sync(self)
+            _la = self._input.LA(1)
+            if _la==TacticNotationsParser.ATOM:
+                self.state = 39
+                self.match(TacticNotationsParser.ATOM)
+
+
+            self.state = 42
+            self.match(TacticNotationsParser.WHITESPACE)
+            self.state = 43
+            self.blocks()
+            self.state = 45
+            self._errHandler.sync(self)
+            _la = self._input.LA(1)
+            if _la==TacticNotationsParser.WHITESPACE:
+                self.state = 44
+                self.match(TacticNotationsParser.WHITESPACE)
+
+
+            self.state = 47
+            self.match(TacticNotationsParser.RBRACE)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class CurliesContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def LBRACE(self):
+            return self.getToken(TacticNotationsParser.LBRACE, 0)
+
+        def blocks(self):
+            return self.getTypedRuleContext(TacticNotationsParser.BlocksContext,0)
+
+
+        def RBRACE(self):
+            return self.getToken(TacticNotationsParser.RBRACE, 0)
+
+        def whitespace(self, i:int=None):
+            if i is None:
+                return self.getTypedRuleContexts(TacticNotationsParser.WhitespaceContext)
+            else:
+                return self.getTypedRuleContext(TacticNotationsParser.WhitespaceContext,i)
+
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_curlies
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitCurlies" ):
+                return visitor.visitCurlies(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def curlies(self):
+
+        localctx = TacticNotationsParser.CurliesContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 8, self.RULE_curlies)
+        self._la = 0 # Token type
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 49
+            self.match(TacticNotationsParser.LBRACE)
+            self.state = 51
+            self._errHandler.sync(self)
+            _la = self._input.LA(1)
+            if _la==TacticNotationsParser.WHITESPACE:
+                self.state = 50
+                self.whitespace()
+
+
+            self.state = 53
+            self.blocks()
+            self.state = 55
+            self._errHandler.sync(self)
+            _la = self._input.LA(1)
+            if _la==TacticNotationsParser.WHITESPACE:
+                self.state = 54
+                self.whitespace()
+
+
+            self.state = 57
+            self.match(TacticNotationsParser.RBRACE)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class WhitespaceContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def WHITESPACE(self):
+            return self.getToken(TacticNotationsParser.WHITESPACE, 0)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_whitespace
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitWhitespace" ):
+                return visitor.visitWhitespace(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def whitespace(self):
+
+        localctx = TacticNotationsParser.WhitespaceContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 10, self.RULE_whitespace)
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 59
+            self.match(TacticNotationsParser.WHITESPACE)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class MetaContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def METACHAR(self):
+            return self.getToken(TacticNotationsParser.METACHAR, 0)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_meta
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitMeta" ):
+                return visitor.visitMeta(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def meta(self):
+
+        localctx = TacticNotationsParser.MetaContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 12, self.RULE_meta)
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 61
+            self.match(TacticNotationsParser.METACHAR)
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class AtomicContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def ATOM(self):
+            return self.getToken(TacticNotationsParser.ATOM, 0)
+
+        def SUB(self):
+            return self.getToken(TacticNotationsParser.SUB, 0)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_atomic
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitAtomic" ):
+                return visitor.visitAtomic(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def atomic(self):
+
+        localctx = TacticNotationsParser.AtomicContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 14, self.RULE_atomic)
+        self._la = 0 # Token type
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 63
+            self.match(TacticNotationsParser.ATOM)
+            self.state = 65
+            self._errHandler.sync(self)
+            _la = self._input.LA(1)
+            if _la==TacticNotationsParser.SUB:
+                self.state = 64
+                self.match(TacticNotationsParser.SUB)
+
+
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
+
+    class HoleContext(ParserRuleContext):
+
+        def __init__(self, parser, parent:ParserRuleContext=None, invokingState:int=-1):
+            super().__init__(parent, invokingState)
+            self.parser = parser
+
+        def ID(self):
+            return self.getToken(TacticNotationsParser.ID, 0)
+
+        def SUB(self):
+            return self.getToken(TacticNotationsParser.SUB, 0)
+
+        def getRuleIndex(self):
+            return TacticNotationsParser.RULE_hole
+
+        def accept(self, visitor:ParseTreeVisitor):
+            if hasattr( visitor, "visitHole" ):
+                return visitor.visitHole(self)
+            else:
+                return visitor.visitChildren(self)
+
+
+
+
+    def hole(self):
+
+        localctx = TacticNotationsParser.HoleContext(self, self._ctx, self.state)
+        self.enterRule(localctx, 16, self.RULE_hole)
+        self._la = 0 # Token type
+        try:
+            self.enterOuterAlt(localctx, 1)
+            self.state = 67
+            self.match(TacticNotationsParser.ID)
+            self.state = 69
+            self._errHandler.sync(self)
+            _la = self._input.LA(1)
+            if _la==TacticNotationsParser.SUB:
+                self.state = 68
+                self.match(TacticNotationsParser.SUB)
+
+
+        except RecognitionException as re:
+            localctx.exception = re
+            self._errHandler.reportError(self, re)
+            self._errHandler.recover(self, re)
+        finally:
+            self.exitRule()
+        return localctx
diff --git a/doc/tools/coqrst/notations/TacticNotationsVisitor.py b/doc/tools/coqrst/notations/TacticNotationsVisitor.py
new file mode 100644
index 00000000..c0bcc4af
--- /dev/null
+++ b/doc/tools/coqrst/notations/TacticNotationsVisitor.py
@@ -0,0 +1,58 @@
+# Generated from TacticNotations.g by ANTLR 4.7
+from antlr4 import *
+if __name__ is not None and "." in __name__:
+    from .TacticNotationsParser import TacticNotationsParser
+else:
+    from TacticNotationsParser import TacticNotationsParser
+
+# This class defines a complete generic visitor for a parse tree produced by TacticNotationsParser.
+
+class TacticNotationsVisitor(ParseTreeVisitor):
+
+    # Visit a parse tree produced by TacticNotationsParser#top.
+    def visitTop(self, ctx:TacticNotationsParser.TopContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#blocks.
+    def visitBlocks(self, ctx:TacticNotationsParser.BlocksContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#block.
+    def visitBlock(self, ctx:TacticNotationsParser.BlockContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#repeat.
+    def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#curlies.
+    def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#whitespace.
+    def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#meta.
+    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#atomic.
+    def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
+        return self.visitChildren(ctx)
+
+
+    # Visit a parse tree produced by TacticNotationsParser#hole.
+    def visitHole(self, ctx:TacticNotationsParser.HoleContext):
+        return self.visitChildren(ctx)
+
+
+
+del TacticNotationsParser
diff --git a/doc/tools/coqrst/notations/__init__.py b/doc/tools/coqrst/notations/__init__.py
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/doc/tools/coqrst/notations/__init__.py
diff --git a/doc/tools/coqrst/notations/fontsupport.py b/doc/tools/coqrst/notations/fontsupport.py
new file mode 100755
index 00000000..a3efd97f
--- /dev/null
+++ b/doc/tools/coqrst/notations/fontsupport.py
@@ -0,0 +1,80 @@
+#!/usr/bin/env python2
+# -*- 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)         ##
+##########################################################################
+"""Transform a font to center each of its characters in square bounding boxes.
+
+See https://stackoverflow.com/questions/37377476/ for background information.
+"""
+
+from collections import Counter
+
+try:
+    import fontforge
+    import psMat
+except ImportError:
+    print("This program requires FontForge's python bindings:")
+    print("  git clone https://github.com/fontforge/fontforge")
+    print("  cd fontforge")
+    print("  ./bootstrap")
+    print("  ./configure")
+    print("  make -j8")
+    print("  sudo make install")
+    raise
+
+def glyph_height(glyph):
+    _, ylo, _, yhi = glyph.boundingBox()
+    return yhi - ylo
+
+def scale_single_glyph(glyph, width, height):
+    """Center glyph in a box of size width*height"""
+    # Some glyphs (such as ‘;’) contain references (‘.’ + ‘,’), and moving the
+    # referenced glyphs moves them in all glyphs that reference them.
+    # Unlinking copies references into this glyph
+    glyph.unlinkThisGlyph()
+    # Width
+    deltaw = width - glyph.width
+    glyph.left_side_bearing += deltaw / 2
+    glyph.right_side_bearing += deltaw - glyph.left_side_bearing
+    glyph.width = width
+    # Height
+    ylo = glyph.boundingBox()[1]
+    deltah = height - glyph_height(glyph)
+    glyph.transform(psMat.translate(0, deltah / 2.0 - ylo))
+
+def avg(lst):
+    lst = list(lst)
+    return sum(lst) / float(len(lst))
+
+def trim_font(fnt):
+    """Remove characters codes beyond 191 front fnt"""
+    for g in fnt.glyphs():
+        if g.unicode >= 191:
+            fnt.removeGlyph(g)
+    return fnt
+
+def center_glyphs(src_font_path, dst_font_path, dst_name):
+    fnt = trim_font(fontforge.open(src_font_path))
+
+    size = max(g.width for g in fnt.glyphs())
+    fnt.ascent, fnt.descent = size, 0
+    for glyph in fnt.glyphs():
+        scale_single_glyph(glyph, size, size)
+
+    fnt.sfnt_names = []
+    fnt.fontname = fnt.familyname = fnt.fullname = dst_name
+    fnt.generate(dst_font_path)
+
+if __name__ == '__main__':
+    from os.path import dirname, join, abspath
+    curdir = dirname(abspath(__file__))
+    ubuntumono_path = join(curdir, "UbuntuMono-B.ttf")
+    ubuntumono_mod_path = join(curdir, "CoqNotations.ttf")
+    center_glyphs(ubuntumono_path, ubuntumono_mod_path, "CoqNotations")
diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py
new file mode 100644
index 00000000..87a41cf9
--- /dev/null
+++ b/doc/tools/coqrst/notations/html.py
@@ -0,0 +1,75 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+"""A visitor for ANTLR notation ASTs, producing raw HTML.
+
+Uses the dominate package.
+"""
+
+from dominate import tags
+
+from .parsing import parse
+from .TacticNotationsParser import TacticNotationsParser
+from .TacticNotationsVisitor import TacticNotationsVisitor
+
+class TacticNotationsToHTMLVisitor(TacticNotationsVisitor):
+    def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
+        with tags.span(_class="repeat-wrapper"):
+            with tags.span(_class="repeat"):
+                self.visitChildren(ctx)
+            repeat_marker = ctx.LGROUP().getText()[1]
+            separator = ctx.ATOM()
+            tags.sup(repeat_marker)
+            if separator:
+                tags.sub(separator.getText())
+
+    def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext):
+        sp = tags.span(_class="curlies")
+        sp.add("{")
+        with sp:
+            self.visitChildren(ctx)
+        sp.add("}")
+
+    def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
+        tags.span(ctx.ATOM().getText())
+
+    def visitHole(self, ctx:TacticNotationsParser.HoleContext):
+        tags.span(ctx.ID().getText()[1:], _class="hole")
+        sub = ctx.SUB()
+        if sub:
+            tags.sub(sub.getText()[1:])
+
+    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+        txt = ctx.METACHAR().getText()[1:]
+        if (txt == "{") or (txt == "}"):
+            tags.span(txt)
+        else:
+            tags.span(txt, _class="meta")
+
+    def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
+        tags.span(" ")          # TODO: no need for a <span> here
+
+def htmlize(notation):
+    """Translate notation to a dominate HTML tree"""
+    top = tags.span(_class='notation')
+    with top:
+        TacticNotationsToHTMLVisitor().visit(parse(notation))
+    return top
+
+def htmlize_str(notation):
+    """Translate notation to a raw HTML document"""
+    # ‘pretty=True’ introduces spurious spaces
+    return htmlize(notation).render(pretty=False)
+
+def htmlize_p(notation):
+    """Like `htmlize`, wrapped in a ‘p’.
+    Does not return: instead, must be run in a dominate context.
+    """
+    with tags.p():
+        htmlize(notation)
diff --git a/doc/tools/coqrst/notations/parsing.py b/doc/tools/coqrst/notations/parsing.py
new file mode 100644
index 00000000..506240d9
--- /dev/null
+++ b/doc/tools/coqrst/notations/parsing.py
@@ -0,0 +1,37 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+from .TacticNotationsLexer import TacticNotationsLexer
+from .TacticNotationsParser import TacticNotationsParser
+
+from antlr4 import CommonTokenStream, InputStream
+
+SUBSTITUTIONS = [#("@bindings_list", "{+ (@id := @val) }"),
+                 ("@qualid_or_string", "@id|@string")]
+
+def substitute(notation):
+    """Perform common substitutions in the notation string.
+
+    Nested notations quickly became unwieldy in the original ‘…’-based format,
+    so they were avoided and replaced by pointers to grammar rules.  With the
+    new format, it's usually nicer to remove the indirection.
+    """
+    for (src, dst) in SUBSTITUTIONS:
+        notation = notation.replace(src, dst)
+    return notation
+
+def parse(notation):
+    """Parse a notation string.
+
+    :return: An ANTLR AST. Use one of the supplied visitors (or write your own)
+             to turn it into useful output.
+    """
+    substituted = substitute(notation)
+    lexer = TacticNotationsLexer(InputStream(substituted))
+    return TacticNotationsParser(CommonTokenStream(lexer)).top()
diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py
new file mode 100644
index 00000000..f6e82fc6
--- /dev/null
+++ b/doc/tools/coqrst/notations/plain.py
@@ -0,0 +1,53 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+"""A visitor for ANTLR notation ASTs, producing plain text with ellipses.
+
+Somewhat-closely approximates the rendering of the original manual.
+"""
+
+from io import StringIO
+
+from .parsing import parse
+from .TacticNotationsParser import TacticNotationsParser
+from .TacticNotationsVisitor import TacticNotationsVisitor
+
+class TacticNotationsToDotsVisitor(TacticNotationsVisitor):
+    def __init__(self):
+        self.buffer = StringIO()
+
+    def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
+        separator = ctx.ATOM()
+        self.visitChildren(ctx)
+        if ctx.LGROUP().getText()[1] == "+":
+            spacer = (separator.getText() + " " if separator else "")
+            self.buffer.write(spacer + "…" + spacer)
+            self.visitChildren(ctx)
+
+    def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext):
+        self.buffer.write("{")
+        self.visitChildren(ctx)
+        self.buffer.write("}")
+
+    def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
+        self.buffer.write(ctx.ATOM().getText())
+
+    def visitHole(self, ctx:TacticNotationsParser.HoleContext):
+        self.buffer.write("‘{}’".format(ctx.ID().getText()[1:]))
+
+    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+        self.buffer.write(ctx.METACHAR().getText()[1:])
+
+    def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
+        self.buffer.write(" ")
+
+def stringify_with_ellipses(notation):
+    vs = TacticNotationsToDotsVisitor()
+    vs.visit(parse(notation))
+    return vs.buffer.getvalue()
diff --git a/doc/tools/coqrst/notations/regexp.py b/doc/tools/coqrst/notations/regexp.py
new file mode 100644
index 00000000..ea820c71
--- /dev/null
+++ b/doc/tools/coqrst/notations/regexp.py
@@ -0,0 +1,60 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+"""An experimental visitor for ANTLR notation ASTs, producing regular expressions."""
+
+import re
+from io import StringIO
+
+from .parsing import parse
+from .TacticNotationsParser import TacticNotationsParser
+from .TacticNotationsVisitor import TacticNotationsVisitor
+
+class TacticNotationsToRegexpVisitor(TacticNotationsVisitor):
+    def __init__(self):
+        self.buffer = StringIO()
+
+    def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
+        separator = ctx.ATOM()
+        repeat_marker = ctx.LGROUP().getText()[1]
+
+        self.buffer.write("(")
+        self.visitChildren(ctx)
+        self.buffer.write(")")
+
+        if repeat_marker in ["?", "*"]:
+            self.buffer.write("?")
+        elif repeat_marker in ["+", "*"]:
+            self.buffer.write("(")
+            self.buffer.write(r"\s*" + re.escape(separator.getText() if separator else " ") + r"\s*")
+            self.visitChildren(ctx)
+            self.buffer.write(")*")
+
+    def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext):
+        self.buffer.write(r"\{")
+        self.visitChildren(ctx)
+        self.buffer.write(r"\}")
+
+    def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
+        self.buffer.write(re.escape(ctx.ATOM().getText()))
+
+    def visitHole(self, ctx:TacticNotationsParser.HoleContext):
+        self.buffer.write("([^();. \n]+)") # FIXME could allow more things
+
+    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+        self.buffer.write(re.escape(ctx.METACHAR().getText()[1:]))
+
+    def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
+        self.buffer.write(r"\s+")
+
+def regexpify(notation):
+    """Translate notation to a Python regular expression matching it"""
+    vs = TacticNotationsToRegexpVisitor()
+    vs.visit(parse(notation))
+    return vs.buffer.getvalue()
diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py
new file mode 100644
index 00000000..e05b8341
--- /dev/null
+++ b/doc/tools/coqrst/notations/sphinx.py
@@ -0,0 +1,102 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+"""A visitor for ANTLR notation ASTs, producing Sphinx nodes.
+
+Unlike the HTML visitor, this produces Sphinx-friendly nodes that can be used by
+all backends. If you just want HTML output, use the HTML visitor.
+"""
+
+from .parsing import parse
+from .TacticNotationsParser import TacticNotationsParser
+from .TacticNotationsVisitor import TacticNotationsVisitor
+
+from docutils import nodes
+from sphinx import addnodes
+
+import sys
+
+class TacticNotationsToSphinxVisitor(TacticNotationsVisitor):
+    def defaultResult(self):
+        return []
+
+    def aggregateResult(self, aggregate, nextResult):
+        if nextResult:
+            aggregate.extend(nextResult)
+        return aggregate
+
+    def visitRepeat(self, ctx:TacticNotationsParser.RepeatContext):
+        # Uses inline nodes instead of subscript and superscript to ensure that
+        # we get the right customization hooks at the LaTeX level
+        wrapper = nodes.inline('', '', classes=['repeat-wrapper'])
+        wrapper += nodes.inline('', '', *self.visitChildren(ctx), classes=["repeat"])
+
+        repeat_marker = ctx.LGROUP().getText()[1]
+        wrapper += nodes.inline(repeat_marker, repeat_marker, classes=['notation-sup'])
+
+        separator = ctx.ATOM()
+        if separator:
+            sep = separator.getText()
+            wrapper += nodes.inline(sep, sep, classes=['notation-sub'])
+
+        return [wrapper]
+
+    def visitCurlies(self, ctx:TacticNotationsParser.CurliesContext):
+        sp = nodes.inline('', '', classes=["curlies"])
+        sp += nodes.Text("{")
+        sp.extend(self.visitChildren(ctx))
+        sp += nodes.Text("}")
+        return [sp]
+
+    def visitAtomic(self, ctx:TacticNotationsParser.AtomicContext):
+        atom = ctx.ATOM().getText()
+        sub = ctx.SUB()
+        node = nodes.inline(atom, atom)
+
+        if sub:
+            sub_index = sub.getText()[2:]
+            node += nodes.subscript(sub_index, sub_index)
+
+        return [node]
+
+    def visitHole(self, ctx:TacticNotationsParser.HoleContext):
+        hole = ctx.ID().getText()
+        token_name = hole[1:]
+        node = nodes.inline(hole, token_name, classes=["hole"])
+
+        sub = ctx.SUB()
+        if sub:
+            sub_index = sub.getText()[2:]
+            node += nodes.subscript(sub_index, sub_index)
+
+        return [addnodes.pending_xref(token_name, node, reftype='token', refdomain='std', reftarget=token_name)]
+
+    def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
+        meta = ctx.METACHAR().getText()
+        metachar = meta[1:] # remove escape char
+        token_name = metachar
+        if (metachar == "{") or (metachar == "}"):
+            classes=[]
+        else:
+            classes=["meta"]
+        return [nodes.inline(metachar, token_name, classes=classes)]
+
+    def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
+        return [nodes.Text(" ")]
+
+def sphinxify(notation):
+    """Translate notation into a Sphinx document tree"""
+    vs = TacticNotationsToSphinxVisitor()
+    return vs.visit(parse(notation))
+
+def main():
+    print(sphinxify("a := {+, b {+ c}}"))
+
+if __name__ == '__main__':
+    main()
diff --git a/doc/tools/coqrst/repl/__init__.py b/doc/tools/coqrst/repl/__init__.py
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/doc/tools/coqrst/repl/__init__.py
diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py
new file mode 100644
index 00000000..495eea91
--- /dev/null
+++ b/doc/tools/coqrst/repl/ansicolors.py
@@ -0,0 +1,99 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+"""
+Parse Coq's ANSI output.
+========================
+
+Translated to Python from Coq's terminal.ml.
+"""
+
+# pylint: disable=too-many-return-statements, too-many-branches
+
+def parse_color(style, offset):
+    color = style[offset] % 10
+    if color == 0:
+        return ("black", 1)
+    elif color == 1:
+        return ("red", 1)
+    elif color == 2:
+        return ("green", 1)
+    elif color == 3:
+        return ("yellow", 1)
+    elif color == 4:
+        return ("blue", 1)
+    elif color == 5:
+        return ("magenta", 1)
+    elif color == 6:
+        return ("cyan", 1)
+    elif color == 7:
+        return ("white", 1)
+    elif color == 9:
+        return ("default", 1)
+    elif color == 8:
+        nxt = style[offset + 1]
+        if nxt == 5:
+            return ("index-{}".format(style[offset + 1]), 2)
+        elif nxt == 2:
+            return ("rgb-{}-{}-{}".format(*style[offset+1:offset+4]), 4)
+        else:
+            raise ValueError("{}, {}".format(style, offset))
+    else:
+        raise ValueError()
+
+def parse_style(style, offset, acc):
+    offset = 0
+    while offset < len(style):
+        head = style[offset]
+
+        if head == 0:
+            acc.append("reset")
+        elif head == 1:
+            acc.append("bold")
+        elif head == 3:
+            acc.append("italic")
+        elif head == 4:
+            acc.append("underline")
+        elif head == 7:
+            acc.append("negative")
+        elif head == 22:
+            acc.append("no-bold")
+        elif head == 23:
+            acc.append("no-italic")
+        elif head == 24:
+            acc.append("no-underline")
+        elif head == 27:
+            acc.append("no-negative")
+        else:
+            color, suboffset = parse_color(style, offset)
+            offset += suboffset - 1
+            if 30 <= head < 40:
+                acc.append("fg-{}".format(color))
+            elif 40 <= head < 50:
+                acc.append("bg-{}".format(color))
+            elif 90 <= head < 100:
+                acc.append("fg-light-{}".format(color))
+            elif 100 <= head < 110:
+                acc.append("bg-light-{}".format(color))
+
+        offset += 1
+
+def parse_ansi(code):
+    """Parse an ansi code into a collection of CSS classes.
+
+    :param code: A sequence of ‘;’-separated ANSI codes.  Do not include the
+                 leading ‘^[[’ or the final ‘m’
+    """
+    classes = []
+    parse_style([int(c) for c in code.split(';')], 0, classes)
+    return ["ansi-" + cls for cls in classes]
+
+if __name__ == '__main__':
+    # As produced by Coq with ‘Check nat.’
+    print(parse_ansi("92;49;22;23;24;27"))
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py
new file mode 100644
index 00000000..aeadce4c
--- /dev/null
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -0,0 +1,103 @@
+##########################################################################
+##         #   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)         ##
+##########################################################################
+"""
+Drive coqtop with Python!
+=========================
+
+This module is a simple pexpect-based driver for coqtop, based on the old
+REPL interface.
+"""
+
+import os
+import re
+
+import pexpect
+
+class CoqTop:
+    """Create an instance of coqtop.
+
+    Use this as a context manager: no instance of coqtop is created until
+    you call `__enter__`.  coqtop is terminated when you `__exit__` the
+    context manager.
+
+    Sentence parsing is very basic for now (a "." in a quoted string will
+    confuse it).
+    """
+
+    COQTOP_PROMPT = re.compile("\r\n[^< ]+ < ")
+
+    def __init__(self, coqtop_bin=None, color=False, args=None) -> str:
+        """Configure a coqtop instance (but don't start it yet).
+
+        :param coqtop_bin: The path to coqtop; uses $COQBIN by default, falling back to "coqtop"
+        :param color:      When True, tell coqtop to produce ANSI color codes (see
+                           the ansicolors module)
+        :param args:       Additional arugments to coqtop.
+        """
+        self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop")
+        if not pexpect.utils.which(self.coqtop_bin):
+            raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin))
+        self.args = (args or []) + ["-boot", "-color", "on"] * color
+        self.coqtop = None
+
+    def __enter__(self):
+        if self.coqtop:
+            raise ValueError("This module isn't re-entrant")
+        self.coqtop = pexpect.spawn(self.coqtop_bin, args=self.args, echo=False, encoding="utf-8")
+        # Disable delays (http://pexpect.readthedocs.io/en/stable/commonissues.html?highlight=delaybeforesend)
+        self.coqtop.delaybeforesend = 0
+        self.next_prompt()
+        return self
+
+    def __exit__(self, type, value, traceback):
+        self.coqtop.kill(9)
+
+    def next_prompt(self):
+        "Wait for the next coqtop prompt, and return the output preceeding it."
+        self.coqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 10)
+        return self.coqtop.before
+
+    def sendone(self, sentence):
+        """Send a single sentence to coqtop.
+
+        :sentence: One Coq sentence (otherwise, Coqtop will produce multiple
+                   prompts and we'll get confused)
+        """
+        # Suppress newlines, but not spaces: they are significant in notations
+        sentence = re.sub(r"[\r\n]+", " ", sentence).strip()
+        self.coqtop.sendline(sentence)
+        try:
+            output = self.next_prompt()
+        except:
+            print("Error while sending the following sentence to coqtop: {}".format(sentence))
+            raise
+        # print("Got {}".format(repr(output)))
+        return output
+
+def sendmany(*sentences):
+    """A small demo: send each sentence in sentences and print the output"""
+    with CoqTop() as coqtop:
+        for sentence in sentences:
+            print("=====================================")
+            print(sentence)
+            print("-------------------------------------")
+            response = coqtop.sendone(sentence)
+            print(response)
+
+def main():
+    """Run a simple performance test and demo `sendmany`"""
+    with CoqTop() as coqtop:
+        for _ in range(200):
+            print(repr(coqtop.sendone("Check nat.")))
+        sendmany("Goal False -> True.", "Proof.", "intros H.",
+                 "Check H.", "Chchc.", "apply I.", "Qed.")
+
+if __name__ == '__main__':
+    main()