Merge PR #7556: Add a setting to warn about empty object in the refman

3 files changed, 126 insertions, 0 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 5f2f21f2b..3036fac81 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -22,6 +22,7 @@ Our Coq domain define multiple `objects`_.  Each object has a *signature* (think
       matching :n:`@pattern` in the current goal.
 
       .. exn:: Too few occurrences
+         :undocumented:
 
 Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```.
 
@@ -31,6 +32,8 @@ Names (link targets) are auto-generated for most simple objects, though they can
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
 - Vernac variants, tactic notations, and tactic variants do not have a default name.
 
+Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.
+
 Notations
 ---------
 
@@ -291,6 +294,64 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
     <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_
     and reference its tokens using ``:token:`…```.
 
+Common mistakes
+===============
+
+Improper nesting
+----------------
+
+DO
+  .. code::
+
+     .. cmd:: Foo @bar
+
+        Foo the first instance of :token:`bar`\ s.
+
+        .. cmdv:: Foo All
+
+           Foo all the :token:`bar`\ s in
+           the current context
+
+DON'T
+  .. code::
+
+     .. cmd:: Foo @bar
+
+     Foo the first instance of :token:`bar`\ s.
+
+     .. cmdv:: Foo All
+
+     Foo all the :token:`bar`\ s in
+     the current context
+
+You can set the ``report_undocumented_coq_objects`` setting in ``conf.py`` to ``"info"`` or ``"warning"`` to get a list of all Coq objects without a description.
+
+Overusing ``:token:``
+---------------------
+
+DO
+  .. code::
+
+     This is equivalent to :n:`Axiom @ident : @term`.
+
+DON'T
+  .. code::
+
+     This is equivalent to ``Axiom`` :token`ident` : :token:`term`.
+
+Omitting annotations
+--------------------
+
+DO
+  .. code::
+
+     .. tacv:: assert @form as @intro_pattern
+
+DON'T
+  .. code::
+
+     .. tacv:: assert form as intro_pattern
+
 Tips and tricks
 ===============
 
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index 203251abf..f90efa995 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -22,6 +22,7 @@ Our Coq domain define multiple `objects`_.  Each object has a *signature* (think
       matching :n:`@pattern` in the current goal.
 
       .. exn:: Too few occurrences
+         :undocumented:
 
 Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```.
 
@@ -31,6 +32,8 @@ Names (link targets) are auto-generated for most simple objects, though they can
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
 - Vernac variants, tactic notations, and tactic variants do not have a default name.
 
+Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.
+
 Notations
 ---------
 
@@ -83,6 +86,64 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
 
 [ROLES]
 
+Common mistakes
+===============
+
+Improper nesting
+----------------
+
+DO
+  .. code::
+
+     .. cmd:: Foo @bar
+
+        Foo the first instance of :token:`bar`\ s.
+
+        .. cmdv:: Foo All
+
+           Foo all the :token:`bar`\ s in
+           the current context
+
+DON'T
+  .. code::
+
+     .. cmd:: Foo @bar
+
+     Foo the first instance of :token:`bar`\ s.
+
+     .. cmdv:: Foo All
+
+     Foo all the :token:`bar`\ s in
+     the current context
+
+You can set the ``report_undocumented_coq_objects`` setting in ``conf.py`` to ``"info"`` or ``"warning"`` to get a list of all Coq objects without a description.
+
+Overusing ``:token:``
+---------------------
+
+DO
+  .. code::
+
+     This is equivalent to :n:`Axiom @ident : @term`.
+
+DON'T
+  .. code::
+
+     This is equivalent to ``Axiom`` :token`ident` : :token:`term`.
+
+Omitting annotations
+--------------------
+
+DO
+  .. code::
+
+     .. tacv:: assert @form as @intro_pattern
+
+DON'T
+  .. code::
+
+     .. tacv:: assert form as intro_pattern
+
 Tips and tricks
 ===============
 
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 1f7dd9d68..f65400e88 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -51,6 +51,10 @@ extensions = [
     'coqrst.coqdomain'
 ]
 
+# Change this to "info" or "warning" to get notifications about undocumented Coq
+# objects (objects with no contents).
+report_undocumented_coq_objects = None
+
 # Add any paths that contain templates here, relative to this directory.
 templates_path = ['_templates']