diff options
| -rw-r--r-- | doc/sphinx/README.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/README.template.rst | 2 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 32de15ee31..30ac2cec80 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -32,7 +32,7 @@ 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. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects):: +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. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: .. cmdv:: Lemma @ident {? @binders} : @type Remark @ident {? @binders} : @type diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index f1d2541eb6..c333d6e9d5 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -32,7 +32,7 @@ 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. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects):: +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. When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes):: .. cmdv:: Lemma @ident {? @binders} : @type Remark @ident {? @binders} : @type diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index c9487abf03..8f135c9185 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -158,7 +158,7 @@ class CoqObject(ObjectDescription): def _add_index_entry(self, name, target): """Add `name` (pointing to `target`) to the main index.""" index_text = name - if self.index_suffix: + if self.index_suffix and not name.startswith("_"): index_text += " " + self.index_suffix self.indexnode['entries'].append(('single', index_text, target, '', None)) |