Define flags (binary-valued settings) and tables (settings that are sets)

as separate NotationObject types, include in index.

5 files changed, 75 insertions, 14 deletions

diff --git a/doc/README.md b/doc/README.md
index cb3427e010..1461fa2e2c 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -103,7 +103,7 @@ to avoid treating Sphinx warnings as errors.  Otherwise, Sphinx quits
 upon detecting the first warning.  You can set this on the Sphinx `make`
 command line or as an environment variable:
 
-- `make sphinx SPINXWARNERROR=0`
+- `make sphinx SPHINXWARNERROR=0`
 
 - ~~~
   export SPHINXWARNERROR=0
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 369a3a0db8..c1f3f7b4d0 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -114,15 +114,33 @@ 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.
 
-``.. opt::`` :black_nib: A Coq option.
+``.. flag::`` :black_nib: A Coq flag (i.e a binary-valued setting).
     Example::
 
-       .. opt:: Nonrecursive Elimination Schemes
+       .. flag:: Nonrecursive Elimination Schemes
 
           This option controls whether types declared with the keywords
           :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
           induction principles.
 
+``.. opt::`` :black_nib: A Coq option (with a string or numeric value; use "flag" for binary options)
+    Example::
+
+       .. opt:: Printing Width @num
+          :name: Printing Width
+
+       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 ...
+
 ``.. prodn::`` A grammar production.
     This is useful if you intend to document individual grammar productions.
     Otherwise, use Sphinx's `production lists
diff --git a/doc/sphinx/coq-exnindex.rst b/doc/sphinx/coq-exnindex.rst
index dbf60bb06c..fc55e91eee 100644
--- a/doc/sphinx/coq-exnindex.rst
+++ b/doc/sphinx/coq-exnindex.rst
@@ -2,6 +2,6 @@
 
 .. hack to get index in TOC
 
-----------------------
-Errors, warnings index
-----------------------
+-------------------------
+Errors and warnings index
+-------------------------
diff --git a/doc/sphinx/coq-optindex.rst b/doc/sphinx/coq-optindex.rst
index 925d4cd185..0961bea61f 100644
--- a/doc/sphinx/coq-optindex.rst
+++ b/doc/sphinx/coq-optindex.rst
@@ -2,6 +2,6 @@
 
 .. hack to get index in TOC
 
------------------
-Option index
------------------
+-------------------------------
+Flags, options and tables index
+-------------------------------
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 2bf9776751..7992c10abb 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -337,11 +337,10 @@ class OptionObject(NotationObject):
 
     Example::
 
-       .. opt:: Nonrecursive Elimination Schemes
+       .. opt:: Hyps Limit @num
 
-          This option controls whether types declared with the keywords
-          :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
-          induction principles.
+          This option controls the maximum number of hypotheses displayed in goals after
+          the application of a tactic.
     """
     subdomain = "opt"
     index_suffix = "(opt)"
@@ -350,6 +349,42 @@ class OptionObject(NotationObject):
     def _name_from_signature(self, signature):
         return stringify_with_ellipses(signature)
 
+
+class FlagObject(NotationObject):
+    """A Coq flag, i.e. a boolean Option.
+
+    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
+          induction principles.
+    """
+    subdomain = "flag"
+    index_suffix = "(flag)"
+    annotation = "Flag"
+
+    def _name_from_signature(self, signature):
+        return stringify_with_ellipses(signature)
+
+
+class TableObject(NotationObject):
+    """A Coq table, i.e. a setting that is a set of values.
+
+    Example::
+
+       .. table:: Search Blacklist
+
+          This table controls ...
+    """
+    subdomain = "table"
+    index_suffix = "(table)"
+    annotation = "Table"
+
+    def _name_from_signature(self, signature):
+        return stringify_with_ellipses(signature)
+
 class ProductionObject(CoqObject):
     r"""A grammar production.
 
@@ -912,7 +947,7 @@ class CoqTacticIndex(CoqSubdomainsIndex):
     name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tacn"]
 
 class CoqOptionIndex(CoqSubdomainsIndex):
-    name, localname, shortname, subdomains = "optindex", "Option Index", "options", ["opt"]
+    name, localname, shortname, subdomains = "optindex", "Flags, options and Tables Index", "options", ["flag", "opt", "table"]
 
 class CoqGallinaIndex(CoqSubdomainsIndex):
     name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"]
@@ -985,6 +1020,8 @@ class CoqDomain(Domain):
         'tacn': ObjType('tacn', 'tacn'),
         'tacv': ObjType('tacv', 'tacn'),
         'opt': ObjType('opt', 'opt'),
+        'flag': ObjType('flag', 'flag'),
+        'table': ObjType('table', 'table'),
         'thm': ObjType('thm', 'thm'),
         'prodn': ObjType('prodn', 'prodn'),
         'exn': ObjType('exn', 'exn'),
@@ -1001,6 +1038,8 @@ class CoqDomain(Domain):
         'tacn': TacticNotationObject,
         'tacv': TacticNotationVariantObject,
         'opt': OptionObject,
+        'flag': FlagObject,
+        'table': TableObject,
         'thm': GallinaObject,
         'prodn' : ProductionObject,
         'exn': ExceptionObject,
@@ -1012,6 +1051,8 @@ class CoqDomain(Domain):
         'cmd': XRefRole(warn_dangling=True),
         'tacn': XRefRole(warn_dangling=True),
         'opt': XRefRole(warn_dangling=True),
+        'flag': XRefRole(warn_dangling=True),
+        'table': XRefRole(warn_dangling=True),
         'thm': XRefRole(warn_dangling=True),
         'prodn' : XRefRole(warn_dangling=True),
         'exn': XRefRole(warn_dangling=True),
@@ -1033,6 +1074,8 @@ class CoqDomain(Domain):
             'cmd': {},
             'tacn': {},
             'opt': {},
+            'flag': {},
+            'table': {},
             'thm': {},
             'prodn' : {},
             'exn': {},