Merge PR #8541: Update flag, option and table descriptions in coqdomain.py, update README.rst to match.

2 files changed, 27 insertions, 26 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index c1f3f7b4d0..904945a58d 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -114,32 +114,23 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
 
              Raised if :n:`@tactic` does not fully solve the goal.
 
-``.. flag::`` :black_nib: A Coq flag (i.e a binary-valued setting).
+``.. flag::`` :black_nib: A Coq flag (i.e. a boolean setting).
     Example::
 
        .. flag:: Nonrecursive Elimination Schemes
 
-          This option controls whether types declared with the keywords
-          :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
+          Controls whether types declared with the keywords
+          :cmd:`Variant` and :cmd:`Record` get an automatic declaration of
           induction principles.
 
-``.. opt::`` :black_nib: A Coq option (with a string or numeric value; use "flag" for binary options)
+``.. opt::`` :black_nib: A Coq option (a setting with non-boolean value, e.g. a string or numeric value).
     Example::
 
-       .. opt:: Printing Width @num
-          :name: Printing Width
+       .. opt:: Hyps Limit @num
+          :name Hyps Limit
 
-       This command sets which left-aligned part of the width of the screen is used
-       for display. At the time of writing this documentation, the default value
-       is 78.
-
-``.. table::`` :black_nib: A Coq table (i.e a setting whose value is a set).
-    Example::
-
-       .. table:: Search Blacklist @string
-          :name: Search Blacklist
-
-          This table controls ...
+          Controls the maximum number of hypotheses displayed in goals after
+          application of a tactic.
 
 ``.. prodn::`` A grammar production.
     This is useful if you intend to document individual grammar productions.
@@ -159,6 +150,14 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
         .. prodn:: term += let: @pattern := @term in @term
         .. prodn:: occ_switch ::= { {? + %| - } {* @num } }
 
+``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values.
+    Example::
+
+       .. table:: Search Blacklist @string
+          :name: Search Blacklist
+
+          Controls ...
+
 ``.. tacn::`` :black_nib: A tactic, or a tactic notation.
     Example::
 
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 7992c10abb..97dabbf815 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -333,14 +333,15 @@ class TacticNotationVariantObject(TacticNotationObject):
     annotation = "Variant"
 
 class OptionObject(NotationObject):
-    """A Coq option.
+    """A Coq option (a setting with non-boolean value, e.g. a string or numeric value).
 
     Example::
 
        .. opt:: Hyps Limit @num
+          :name Hyps Limit
 
-          This option controls the maximum number of hypotheses displayed in goals after
-          the application of a tactic.
+          Controls the maximum number of hypotheses displayed in goals after
+          application of a tactic.
     """
     subdomain = "opt"
     index_suffix = "(opt)"
@@ -351,14 +352,14 @@ class OptionObject(NotationObject):
 
 
 class FlagObject(NotationObject):
-    """A Coq flag, i.e. a boolean Option.
+    """A Coq flag (i.e. a boolean setting).
 
     Example::
 
        .. flag:: Nonrecursive Elimination Schemes
 
-          This flag controls whether types declared with the keywords
-          :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
+          Controls whether types declared with the keywords
+          :cmd:`Variant` and :cmd:`Record` get an automatic declaration of
           induction principles.
     """
     subdomain = "flag"
@@ -374,9 +375,10 @@ class TableObject(NotationObject):
 
     Example::
 
-       .. table:: Search Blacklist
+       .. table:: Search Blacklist @string
+          :name: Search Blacklist
 
-          This table controls ...
+          Controls ...
     """
     subdomain = "table"
     index_suffix = "(table)"
@@ -1192,6 +1194,6 @@ def setup(app):
     # contents of ``env.domaindata['coq']`` change.  See
     # `https://github.com/sphinx-doc/sphinx/issues/4460`.
     meta = { "version": "0.1",
-             "env_version": 1,
+             "env_version": 2,
              "parallel_read_safe": True }
     return meta