diff options
| author | Théo Zimmermann | 2018-07-25 15:08:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-07-25 18:40:22 +0200 |
| commit | aee50066c9ef94ec2967e2f6f659ecb7a0f9598e (patch) | |
| tree | 36ce371524c40e6a7e9f850942065d75f3232089 /doc/sphinx | |
| parent | 9b6ce4f1848c546d0d361aa1089fa2907ca4c9ad (diff) | |
[sphinx] Add a way of skipping names in the indexes.
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/README.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/README.template.rst | 2 |
2 files changed, 2 insertions, 2 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 |