16 files changed, 77 insertions, 26 deletions
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/03-notations/11986-float-low-level-printing.rst b/doc/changelog/03-notations/11986-float-low-level-printing.rst
new file mode 100644
index 0000000000..f3d85cadc6
--- /dev/null
+++ b/doc/changelog/03-notations/11986-float-low-level-printing.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Add flag ``Printing Float`` to print primitive floats as hexadecimal
+  instead of decimal values. This is included in ``Set Printing All``.
+  (`#11986 <https://github.com/coq/coq/pull/11986>`_,
+  by Pierre Roux).
diff --git a/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst b/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst
new file mode 100644
index 0000000000..2f8d92fae5
--- /dev/null
+++ b/doc/changelog/05-tactic-language/11981-ltac2-eval-notations.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Ltac2 notations for reductions in terms: :n:`eval @red_expr in @ltac2_term`
+  (`#11981 <https://github.com/coq/coq/pull/11981>`_,
+  by Michael Soegtrop).
diff --git a/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst b/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst
new file mode 100644
index 0000000000..259253ec79
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12295-master+fix12234-show-proof.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  A printing bug in the presence of elimination principles with local definitions
+  (`#12295 <https://github.com/coq/coq/pull/12295>`_,
+  by Hugo Herbelin; fixes `#12233 <https://github.com/coq/coq/pull/12233>`_).
diff --git a/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst
new file mode 100644
index 0000000000..5b35090d7e
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12358-redirect_printing_params.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  :cmd:Redirect now obeys the :opt:`Printing Width` and
+  :opt:`Printing Depth` flags.
+  (`#12358 <https://github.com/coq/coq/pull/12358>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/08-tools/12076-fix-5030.rst b/doc/changelog/08-tools/12076-fix-5030.rst
new file mode 100644
index 0000000000..afb59b1cde
--- /dev/null
+++ b/doc/changelog/08-tools/12076-fix-5030.rst
@@ -0,0 +1,4 @@
+- **Fixed:**
+  Fix #5030 (coqchk reports names from opaque modules as axioms)
+  (`#12076 <https://github.com/coq/coq/pull/12076>`_,
+  by Pierre Roux).
diff --git a/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst b/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst
new file mode 100644
index 0000000000..8a43f5af94
--- /dev/null
+++ b/doc/changelog/08-tools/12368-fix-missing-newline-time-file-maker.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  The pretty-timed scripts and targets now print a newline at the end of their
+  tables, rather than creating text with no trailing newline (`#12368
+  <https://github.com/coq/coq/pull/12368>`_, by Jason Gross).
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/changes.rst b/doc/sphinx/changes.rst
index 5954ded67f..363148e2a0 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -147,7 +147,7 @@ Changes in 8.11+beta1
   dropped when forcing a delayed opaque proof inside a polymorphic section. Also
   relaxes the nesting criterion for sections, as polymorphic sections can now
   appear inside a monomorphic one
-  (`#10664, <https://github.com/coq/coq/pull/10664>`_ by Pierre-Marie Pédrot).
+  (`#10664 <https://github.com/coq/coq/pull/10664>`_, by Pierre-Marie Pédrot).
 - **Changed:**
   Using ``SProp`` is now allowed by default, without needing to pass
   ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811
@@ -476,7 +476,7 @@ Changes in 8.11+beta1
   by Vincent Laporte).
 - **Removed:**
   Deprecated modules `Coq.ZArith.Zlogarithm` and `Coq.ZArith.Zsqrt_compat`
-  (`#9881 <https://github.com/coq/coq/pull/9811>`_,
+  (`#9811 <https://github.com/coq/coq/pull/9811>`_,
   by Vincent Laporte).
 
   .. _811Reals:
@@ -690,7 +690,7 @@ Changes in 8.11.1
   Bump official OCaml support and CI testing to 4.10.0
   (`#11131 <https://github.com/coq/coq/pull/11131>`_,
   `#11123 <https://github.com/coq/coq/pull/11123>`_,
-  `#11102 <https://github.com/coq/coq/pull/11123>`_,
+  `#11102 <https://github.com/coq/coq/pull/11102>`_,
   by Emilio Jesus Gallego Arias, Jacques-Henri Jourdan,
   Guillaume Melquiond, and Guillaume Munch-Maccagnoni).
 
@@ -1091,7 +1091,7 @@ Other changes in 8.10+beta1
     e.g., a numeral notation whose parsing function outputs a proof of
     :g:`Nat.gcd x y = 1` will no longer fail to parse due to containing the
     constant :g:`Nat.gcd` in the parameter-argument of :g:`eq_refl`)
-    (`#9874 <https://github.com/coq/coq/pull/9840>`_,
+    (`#9874 <https://github.com/coq/coq/pull/9874>`_,
     closes `#9840 <https://github.com/coq/coq/issues/9840>`_
     and `#9844 <https://github.com/coq/coq/issues/9844>`_,
     by Jason Gross).
@@ -1107,7 +1107,7 @@ Other changes in 8.10+beta1
 
   - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar`
     (`#10061 <https://github.com/coq/coq/pull/10061>`_,
-    fixes `#9681 <http://github.com/coq/coq/pull/9681>`_,
+    fixes `#9681 <https://github.com/coq/coq/pull/9681>`_,
     by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin).
 
 - The `quote plugin
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/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 899173a83a..b2b68482ef 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -1062,11 +1062,17 @@ Floating-point constants are parsed and pretty-printed as (17-digit)
 decimal constants. This ensures that the composition
 :math:`\text{parse} \circ \text{print}` amounts to the identity.
 
-.. warn:: The constant @numeral is not a binary64 floating-point value.  A closest value will be used and unambiguously printed @numeral. [inexact-float,parsing]
+.. warn:: The constant @numeral is not a binary64 floating-point value.  A closest value @numeral will be used and unambiguously printed @numeral. [inexact-float,parsing]
 
    Not all decimal constants are floating-point values. This warning
    is generated when parsing such a constant (for instance ``0.1``).
 
+.. flag:: Printing Float
+
+   Turn this flag off (it is on by default) to deactivate decimal
+   printing of floating-point constants. They will then be printed
+   with an hexadecimal representation.
+
 .. example::
 
   .. coqtop:: all
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/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 1a02d6e65d..ab615d5f65 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -707,5 +707,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Compat/Coq810.v
     theories/Compat/Coq811.v
     theories/Compat/Coq812.v
+    theories/Compat/Coq813.v
   </dd>
 </dl>
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)