6 files changed, 33 insertions, 23 deletions
diff --git a/doc/README.md b/doc/README.md
index 8e1bc85c49..99d285320d 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -28,9 +28,10 @@ Dependencies
 
 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:
+reference manual requires Python 3, and the following Python packages
+(note the version constraints on Sphinx):
 
-  - sphinx >= 2.3.1
+  - sphinx >= 2.3.1 & < 3.0.0
   - sphinx_rtd_theme >= 0.4.3
   - beautifulsoup4 >= 4.0.6
   - antlr4-python3-runtime >= 4.7.1
@@ -40,8 +41,8 @@ reference manual requires Python 3, and the following Python packages:
 To install them, you should first install pip and setuptools (for instance,
 with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run:
 
-    pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime \
-                 pexpect sphinxcontrib-bibtex
+    pip3 install sphinx==2.3.1 sphinx_rtd_theme beautifulsoup4 \
+                 antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex
 
 Nix users should get the correct development environment to build the
 HTML documentation from Coq's [`default.nix`](../default.nix) (note this
@@ -58,7 +59,6 @@ additional tools are required:
   - makeindex
   - xelatex
   - latexmk
-  - xindy
 
 All of them are part of the TexLive distribution. E.g. on Debian / Ubuntu,
 install them with:
@@ -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 fonts-freefont-otf
+                latexmk fonts-freefont-otf
 
 Compilation
 -----------
diff --git a/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst b/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst
deleted file mode 100644
index 8f126c5b6f..0000000000
--- a/doc/changelog/02-specification-language/12422-master+fix-12418-cases-anomaly.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Fixed:**
-  Case of an anomaly in trying to infer the return clause of an ill-typed :g:`match`
-  (`#12422 <https://github.com/coq/coq/pull/12422>`_,
-  fixes `#12418 <https://github.com/coq/coq/pull/12418>`_,
-  by Hugo Herbelin).
diff --git a/doc/changelog/07-commands-and-options/11972-fix-require-in-section.rst b/doc/changelog/07-commands-and-options/11972-fix-require-in-section.rst
deleted file mode 100644
index 7e34c4a0ff..0000000000
--- a/doc/changelog/07-commands-and-options/11972-fix-require-in-section.rst
+++ /dev/null
@@ -1,5 +0,0 @@
-- **Changed:** The warning when using :cmd:`Require` inside a section
-  moved from the ``deprecated`` category to the ``fragile`` category,
-  because there is no plan to remove the functionality at this time.
-  (`#11972 <https://github.com/coq/coq/pull/11972>`_, by Gaëtan
-  Gilbert).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 72f0fdf4c5..0f2fce522a 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -76,6 +76,11 @@ Specification language, type inference
   Anomaly which could be raised when printing binders with implicit types
   (`#12323 <https://github.com/coq/coq/pull/12323>`_,
   by Hugo Herbelin; fixes `#12322 <https://github.com/coq/coq/pull/12322>`_).
+- **Fixed:**
+  Case of an anomaly in trying to infer the return clause of an ill-typed :g:`match`
+  (`#12422 <https://github.com/coq/coq/pull/12422>`_,
+  fixes `#12418 <https://github.com/coq/coq/pull/12418>`_,
+  by Hugo Herbelin).
 
 Notations
 ^^^^^^^^^
@@ -440,6 +445,11 @@ Commands
   Several commands (:cmd:`Search`, :cmd:`About`, ...) now print the
   implicit arguments in brackets when printing types (`#11795
   <https://github.com/coq/coq/pull/11795>`_, by Simon Boulier).
+- **Changed:** The warning when using :cmd:`Require` inside a section
+  moved from the ``deprecated`` category to the ``fragile`` category,
+  because there is no plan to remove the functionality at this time
+  (`#11972 <https://github.com/coq/coq/pull/11972>`_, by Gaëtan
+  Gilbert).
 - **Changed:**
   :cmd:`Redirect` now obeys the :opt:`Printing Width` and
   :opt:`Printing Depth` options
@@ -970,8 +980,14 @@ Infrastructure and dependencies
 
 - **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+
+  now requires Sphinx >= 2.3.1 & < 3.0.0, sphinx_rtd_theme 0.4.3+ and
+  sphinxcontrib-bibtex 0.4.2+.
+
+  .. warning::
+
+     The reference manual is known not to build properly with
+     Sphinx 3.
+
   (`#12224 <https://github.com/coq/coq/pull/12224>`_,
   by Jim Fehrle and Théo Zimmermann).
 - **Removed:**
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index fabf7a519f..99762c7a0e 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -214,11 +214,12 @@ html_context = {
     'conf_py_path': '/doc/sphinx/',
     # Versions and downloads listed in the versions menu (see _templates/versions.html)
     'versions': [
-        ("master", "https://coq.github.io/doc/master/refman/"),
+        ("dev", "https://coq.github.io/doc/master/refman/"),
         ("stable", "https://coq.inria.fr/distrib/current/refman/"),
-        ("v8.11", "https://coq.github.io/doc/v8.11/refman/"),
-        ("v8.10", "https://coq.github.io/doc/v8.10/refman/"),
-        ("v8.9", "https://coq.github.io/doc/v8.9/refman/"),
+        ("v8.12", "https://coq.github.io/doc/v8.12/refman/"),
+        ("8.11", "https://coq.inria.fr/distrib/V8.11.2/refman/"),
+        ("8.10", "https://coq.inria.fr/distrib/V8.10.2/refman/"),
+        ("8.9", "https://coq.inria.fr/distrib/V8.9.1/refman/"),
         ("8.8", "https://coq.inria.fr/distrib/V8.8.2/refman/"),
         ("8.7", "https://coq.inria.fr/distrib/V8.7.2/refman/"),
         ("8.6", "https://coq.inria.fr/distrib/V8.6.1/refman/"),
@@ -356,6 +357,9 @@ latex_elements = {
 
 latex_engine = "xelatex"
 
+# Cf. https://github.com/sphinx-doc/sphinx/issues/7015
+latex_use_xindy = False
+
 ########
 # done #
 ########
diff --git a/doc/sphinx/dune b/doc/sphinx/dune
index b788fbbeed..31f28635fe 100644
--- a/doc/sphinx/dune
+++ b/doc/sphinx/dune
@@ -1,4 +1,4 @@
-(dirs :standard _static)
+(dirs :standard _static _templates)
 
 (rule
  (targets README.gen.rst)