10 files changed, 52 insertions, 29 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f26804e120..4139a0dbe5 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -18,7 +18,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2020-05-06-V70"
+  CACHEKEY: "bionic_coq-V2020-05-18-V3"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -366,12 +366,11 @@ pkg:opam:
   dependencies: []
   script:
     - set -e
-    - opam pin add --kind=path coq.$COQ_VERSION .
-    - opam pin add --kind=path coqide-server.$COQ_VERSION .
-    - opam pin add --kind=path coqide.$COQ_VERSION .
+    - opam pin add --kind=path coq.dev .
+    - opam pin add --kind=path coqide-server.dev .
+    - opam pin add --kind=path coqide.dev .
     - set +e
   variables:
-    COQ_VERSION: "8.13"
     OPAM_SWITCH: "edge"
     OPAM_VARIANT: "+flambda"
   only: *full-ci
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index d5c6096100..801e29ac95 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -179,6 +179,11 @@ but if you wish to save more time you can skip the job by setting
 
 This means you will need to change its value when the Docker image
 needs to be updated. You can do so for a single pipeline by starting
-it through the web interface.
+it through the web interface. Here is a direct link that you can use
+to trigger such a build:
+`https://gitlab.com/coq/coq/pipelines/new?var[SKIP_DOCKER]=false&ref=pr-XXXXX`.
+Note that this link will give a 404 error if you are not logged in or
+a member of the Coq organization on GitLab.  To request to join the
+Coq organization, go to https://gitlab.com/coq to request access.
 
 See also [`docker/README.md`](docker/README.md).
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 9ee6496ee5..51a602303a 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-05-06-V70"
+# CACHEKEY: "bionic_coq-V2020-05-18-V3"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -14,12 +14,13 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         # Dependencies of stdlib and sphinx doc
         texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
         xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
+        fonts-freefont-otf \
         # Dependencies of source-doc and coq-makefile
         texlive-science tipa
 
 # More dependencies of the sphinx doc
-RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \
-                 antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
+RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \
+                 antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2
 
 # We need to install OPAM 2.0 manually for now.
 RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
diff --git a/doc/README.md b/doc/README.md
index e749bcf5d1..8e1bc85c49 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -30,12 +30,12 @@ To produce the complete documentation in HTML, you will need Coq dependencies
 listed in [`INSTALL.md`](../INSTALL.md). Additionally, the Sphinx-based
 reference manual requires Python 3, and the following Python packages:
 
-  - sphinx >= 1.8.0
-  - sphinx_rtd_theme >= 0.2.5b2
+  - sphinx >= 2.3.1
+  - sphinx_rtd_theme >= 0.4.3
   - beautifulsoup4 >= 4.0.6
   - antlr4-python3-runtime >= 4.7.1
   - pexpect >= 4.2.1
-  - sphinxcontrib-bibtex >= 0.4.0
+  - sphinxcontrib-bibtex >= 0.4.2
 
 To install them, you should first install pip and setuptools (for instance,
 with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run:
@@ -68,7 +68,7 @@ install them with:
 Or if you want to use less disk space:
 
     apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
-                latexmk xindy
+                latexmk xindy fonts-freefont-otf
 
 Compilation
 -----------
diff --git a/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst b/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst
new file mode 100644
index 0000000000..35a618ea8d
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/12224-gdef_alias.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  Minimal versions of dependencies for building the reference manual:
+  now requires Sphinx 2.3.1+, sphinx_rtd_theme 0.4.3+ and
+  sphinxcontrib-bibtex 0.4.2+
+  (`#12224 <https://github.com/coq/coq/pull/12224>`_,
+  by Jim Fehrle and Théo Zimmermann).
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index e20469bb8b..f91874d74d 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -359,11 +359,14 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
     and reference its tokens using ``:token:`…```.
 
 ``:gdef:`` Marks the definition of a glossary term inline in the text.  Matching :term:`XXX`
-    constructs will link to it.  The term will also appear in the Glossary Index.
+    constructs will link to it.  Use the form :gdef:`text <term>` to display "text"
+    for the definition of "term", such as when "term" must be capitalized or plural
+    for grammatical reasons.  The term will also appear in the Glossary Index.
 
-    Example::
+    Examples::
 
        A :gdef:`prime` number is divisible only by itself and 1.
+       :gdef:`Composite <composite>` numbers are the non-prime numbers.
 
 Common mistakes
 ===============
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 4136b406de..fabf7a519f 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -46,7 +46,7 @@ with open("refman-preamble.rst") as s:
 # -- General configuration ------------------------------------------------
 
 # If your documentation needs a minimal Sphinx version, state it here.
-needs_sphinx = '1.8.0'
+needs_sphinx = '2.3.1'
 
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 250a0f0326..68900aa0be 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -267,7 +267,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
      Intuitively, types may be viewed as sets containing terms.  We
      say that a type is :gdef:`inhabited` if it contains at least one
      term (i.e. if we can find a term which is associated with this
-     type).  We call such terms :gdef:`witness`\es.  Note that deciding
+     type).  We call such terms :gdef:`witnesses <witness>`.  Note that deciding
      whether a type is inhabited is `undecidable
      <https://en.wikipedia.org/wiki/Undecidable_problem>`_.
 
diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst
index 8307a02d6d..03581b95dd 100644
--- a/doc/sphinx/language/core/sorts.rst
+++ b/doc/sphinx/language/core/sorts.rst
@@ -22,7 +22,7 @@ Sorts
    | @universe_expr
    universe_expr ::= @universe_name {? + @num }
 
-The types of types are called :gdef:`sort`\s.
+The types of types are called :gdef:`sorts <sort>`.
 
 All sorts have a type and there is an infinite well-founded typing
 hierarchy of sorts whose base sorts are :math:`\SProp`, :math:`\Prop`
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index df11960403..e59f694aa7 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -27,13 +27,13 @@ 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, get_node_location
 from sphinx.directives import ObjectDescription
 from sphinx.domains import Domain, ObjType, Index
-from sphinx.domains.std import token_xrefs
+from sphinx.errors import ExtensionError
+from sphinx.roles import XRefRole
+from sphinx.util.docutils import ReferenceRole
+from sphinx.util.logging import getLogger, get_node_location
+from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode
 
 from . import coqdoc
 from .repl import ansicolors
@@ -1162,25 +1162,34 @@ GrammarProductionRole.role_name = "production"
 
 def GlossaryDefRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
     """Marks the definition of a glossary term inline in the text.  Matching :term:`XXX`
-    constructs will link to it.  The term will also appear in the Glossary Index.
+    constructs will link to it.  Use the form :gdef:`text <term>` to display "text"
+    for the definition of "term", such as when "term" must be capitalized or plural
+    for grammatical reasons.  The term will also appear in the Glossary Index.
 
-    Example::
+    Examples::
 
        A :gdef:`prime` number is divisible only by itself and 1.
+       :gdef:`Composite <composite>` numbers are the non-prime numbers.
     """
     #pylint: disable=dangerous-default-value, unused-argument
     env = inliner.document.settings.env
     std = env.domaindata['std']['objects']
-    key = ('term', text)
+    m = ReferenceRole.explicit_title_re.match(text)
+    if m:
+        (text, term) = m.groups()
+        text = text.strip()
+    else:
+        term = text
+    key = ('term', term)
 
     if key in std:
         MSG = 'Duplicate object: {}; other is at {}'
-        msg = MSG.format(text, env.doc2path(std[key][0]))
+        msg = MSG.format(term, env.doc2path(std[key][0]))
         inliner.document.reporter.warning(msg, line=lineno)
 
-    targetid = nodes.make_id('term-{}'.format(text))
+    targetid = nodes.make_id('term-{}'.format(term))
     std[key] = (env.docname, targetid)
-    target = nodes.target('', '', ids=[targetid], names=[text])
+    target = nodes.target('', '', ids=[targetid], names=[term])
     inliner.document.note_explicit_target(target)
     node = nodes.inline(rawtext, '', target, nodes.Text(text), classes=['term-defn'])
     set_role_source_info(inliner, lineno, node)