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

as separate NotationObject types, include in index.

1 files changed, 48 insertions, 5 deletions

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': {},