From 7cac115647723f8261b7aabf8094572227b25c43 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 18 May 2020 18:55:59 +0200 Subject: Bump minimal versions of refman dependencies. Fixes #11936. Co-authored-by: Jim Fehrle --- doc/sphinx/conf.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx') 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 -- cgit v1.2.3 From ae208f062d15773781cb600e9a7b2c44de25caf9 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Thu, 30 Apr 2020 16:51:08 -0700 Subject: Support :gdef:`text ` syntax (adding "") --- doc/sphinx/README.rst | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'doc/sphinx') 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 ` 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 ` numbers are the non-prime numbers. Common mistakes =============== -- cgit v1.2.3 From c1125bda507137c35400808c6de19acfcece0ec7 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 16 May 2020 16:19:59 +0200 Subject: Use the new gdef alt-text feature in the refman. --- doc/sphinx/language/core/basic.rst | 2 +- doc/sphinx/language/core/sorts.rst | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/sphinx') 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 ` 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 `. Note that deciding whether a type is inhabited is `undecidable `_. 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 `. All sorts have a type and there is an infinite well-founded typing hierarchy of sorts whose base sorts are :math:`\SProp`, :math:`\Prop` -- cgit v1.2.3