From a454d1dc509aae06eadf7474eb25e90abdf36ca1 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 23 Sep 2018 22:17:25 -0700
Subject: Update flag, option and table descriptions in coqdomain.py, update
 README.rst to match. Bump env_version.

---
 doc/tools/coqrst/coqdomain.py | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

(limited to 'doc/tools')

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
-- 
cgit v1.2.3