6 files changed, 20 insertions, 11 deletions
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`