diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 3 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 16 |
2 files changed, 11 insertions, 8 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 09090ce89a..721c7a7a51 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1063,6 +1063,9 @@ Parameterized inductive types | cons3 : A -> list3 -> list3. End list3. + Attributes ``uniform`` and ``nonuniform`` respectively enable and + disable uniform parameters for a single inductive declaration block. + .. seealso:: Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 1f9178f4b6..85d86bed62 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -270,7 +270,7 @@ class GallinaObject(PlainObject): :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. """ subdomain = "thm" - index_suffix = "(thm)" + index_suffix = "(theorem)" annotation = "Theorem" class VernacObject(NotationObject): @@ -283,7 +283,7 @@ class VernacObject(NotationObject): This command is equivalent to :n:`…`. """ subdomain = "cmd" - index_suffix = "(cmd)" + index_suffix = "(command)" annotation = "Command" def _name_from_signature(self, signature): @@ -306,7 +306,7 @@ class VernacVariantObject(VernacObject): This is equivalent to :n:`Axiom @ident : @term`. """ - index_suffix = "(cmdv)" + index_suffix = "(command variant)" annotation = "Variant" def _name_from_signature(self, signature): @@ -322,7 +322,7 @@ class TacticNotationObject(NotationObject): :token:`expr` is evaluated to ``v`` which must be a tactic value. … """ subdomain = "tacn" - index_suffix = "(tacn)" + index_suffix = "(tactic)" annotation = None class TacticNotationVariantObject(TacticNotationObject): @@ -342,7 +342,7 @@ class TacticNotationVariantObject(TacticNotationObject): The number is the failure level. If no level is specified, it defaults to 0. … """ - index_suffix = "(tacnv)" + index_suffix = "(tactic variant)" annotation = "Variant" class OptionObject(NotationObject): @@ -357,7 +357,7 @@ class OptionObject(NotationObject): application of a tactic. """ subdomain = "opt" - index_suffix = "(opt)" + index_suffix = "(option)" annotation = "Option" def _name_from_signature(self, signature): @@ -534,7 +534,7 @@ class ExceptionObject(NotationObject): Raised if :n:`@tactic` does not fully solve the goal. """ subdomain = "exn" - index_suffix = "(err)" + index_suffix = "(error)" annotation = "Error" # Uses “exn” since “err” already is a CSS class added by “writer_aux”. @@ -557,7 +557,7 @@ class WarningObject(NotationObject): valid coercion paths are ignored. """ subdomain = "warn" - index_suffix = "(warn)" + index_suffix = "(warning)" annotation = "Warning" # Generate names automatically |