diff options
-rw-r--r-- | doc/sphinx/README.rst | 11 | ||||
-rw-r--r-- | doc/sphinx/README.template.rst | 11 | ||||
-rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 20 | ||||
-rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 | ||||
-rw-r--r-- | doc/tools/coqrst/coqdomain.py | 16 |
5 files changed, 42 insertions, 18 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 3036fac81..35a605ddd 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -32,7 +32,16 @@ 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. +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):: + + .. cmdv:: Lemma @ident {? @binders} : @type + Remark @ident {? @binders} : @type + Fact @ident {? @binders} : @type + Corollary @ident {? @binders} : @type + Proposition @ident {? @binders} : @type + :name: Lemma; Remark; Fact; Corollary; Proposition + + These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. Notations --------- diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index f90efa995..f1d2541eb 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -32,7 +32,16 @@ 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. +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):: + + .. cmdv:: Lemma @ident {? @binders} : @type + Remark @ident {? @binders} : @type + Fact @ident {? @binders} : @type + Corollary @ident {? @binders} : @type + Proposition @ident {? @binders} : @type + :name: Lemma; Remark; Fact; Corollary; Proposition + + These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. Notations --------- diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 76a016ff6..d3d515949 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1266,22 +1266,14 @@ Chapter :ref:`Tactics`. The basic assertion command is: This feature, called nested proofs, is disabled by default. To activate it, turn option :opt:`Nested Proofs Allowed` on. - The following commands are synonyms of :n:`Theorem @ident {? @binders } : type`: - .. cmdv:: Lemma @ident {? @binders } : @type - :name: Lemma - - .. cmdv:: Remark @ident {? @binders } : @type - :name: Remark - - .. cmdv:: Fact @ident {? @binders } : @type - :name: Fact - - .. cmdv:: Corollary @ident {? @binders } : @type - :name: Corollary + Remark @ident {? @binders } : @type + Fact @ident {? @binders } : @type + Corollary @ident {? @binders } : @type + Proposition @ident {? @binders } : @type + :name: Lemma; Remark; Fact; Corollary; Proposition - .. cmdv:: Proposition @ident {? @binders } : @type - :name: Proposition + These commands are all synonyms of :n:`Theorem @ident {? @binders } : type`. .. cmdv:: Theorem @ident : @type {* with @ident : @type} diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 2b128b98f..88c1e225f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -178,7 +178,7 @@ Sequence A sequence is an expression of the following form: .. tacn:: @expr ; @expr - :name: ; + :name: ltac-seq The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be a tactic value. The tactic :n:`v__1` is applied to the current goal, diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 8d6e23764..ab3a485b2 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -118,7 +118,7 @@ class CoqObject(ObjectDescription): annotation = self.annotation + ' ' signode += addnodes.desc_annotation(annotation, annotation) self._render_signature(signature, signode) - return self.options.get("name") or self._name_from_signature(signature) + return self._names.get(signature) or self._name_from_signature(signature) def _record_name(self, name, target_id): """Record a name, mapping it to target_id @@ -176,8 +176,22 @@ class CoqObject(ObjectDescription): if report == "warning": raise self.warning(msg) + def _prepare_names(self): + sigs = self.get_signatures() + names = self.options.get("name") + if names is None: + self._names = {} + else: + names = [n.strip() for n in names.split(";")] + if len(names) != len(sigs): + ERR = ("Expected {} semicolon-separated names, got {}. " + + "Please provide one name per signature line.") + raise self.error(ERR.format(len(names), len(sigs))) + self._names = dict(zip(sigs, names)) + def run(self): self._warn_if_undocumented() + self._prepare_names() return super().run() class PlainObject(CoqObject): |