From 9811cda7698652b51e8ebdb25db7285ab8e5ae9a Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Sun, 13 May 2018 12:18:38 -0400 Subject: [doc] Document the new report_undocumented_coq_objects setting --- doc/sphinx/README.rst | 5 +++++ doc/sphinx/README.template.rst | 5 +++++ 2 files changed, 10 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index eae5c71f9c..3036fac815 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 --------- @@ -321,6 +324,8 @@ DON'T 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:`` --------------------- diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index b51421e2ae..f90efa9958 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 --------- @@ -113,6 +116,8 @@ DON'T 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:`` --------------------- -- cgit v1.2.3