Merge PR #12224: Support :gdef:`text<term>` syntax (adding "<term>")

Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel

4 files changed, 8 insertions, 5 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/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`