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

1 files changed, 16 insertions, 17 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::