Clean-up around cmd documentation.

In particular, remove trailing dots.

7 files changed, 50 insertions, 50 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 1bac87451..cb93d48a4 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -37,11 +37,11 @@ Generating ML Code
 The next two commands are meant to be used for rapid preview of
 extraction. They both display extracted term(s) inside |Coq|.
 
-.. cmd:: Extraction @qualid.
+.. cmd:: Extraction @qualid
 
    Extraction of the mentioned object in the |Coq| toplevel.
 
-.. cmd:: Recursive Extraction @qualid ... @qualid.
+.. cmd:: Recursive Extraction {+ @qualid }
 
    Recursive extraction of all the mentioned objects and
    all their dependencies in the |Coq| toplevel.
@@ -49,7 +49,7 @@ extraction. They both display extracted term(s) inside |Coq|.
 All the following commands produce real ML files. User can choose to
 produce one monolithic file or one file per |Coq| library.
 
-.. cmd:: Extraction "@file" @qualid ... @qualid.
+.. cmd:: Extraction "@file" {+ @qualid }
 
    Recursive extraction of all the mentioned objects and all
    their dependencies in one monolithic `file`.
@@ -57,19 +57,19 @@ produce one monolithic file or one file per |Coq| library.
    language to fulfill its syntactic conventions, keeping original
    names as much as possible.
   
-.. cmd:: Extraction Library @ident.
+.. cmd:: Extraction Library @ident
 
    Extraction of the whole |Coq| library ``ident.v`` to an ML module
    ``ident.ml``. In case of name clash, identifiers are here renamed
    using prefixes ``coq_``  or ``Coq_`` to ensure a session-independent
    renaming.
 
-.. cmd:: Recursive Extraction Library @ident.
+.. cmd:: Recursive Extraction Library @ident
 
    Extraction of the |Coq| library ``ident.v`` and all other modules 
    ``ident.v`` depends on.
 
-.. cmd:: Separate Extraction @qualid ... @qualid.
+.. cmd:: Separate Extraction {+ @qualid }
 
    Recursive extraction of all the mentioned objects and all
    their dependencies, just as ``Extraction "file"``,
@@ -86,7 +86,7 @@ The following command is meant to help automatic testing of
 the extraction, see for instance the ``test-suite`` directory
 in the |Coq| sources.
 
-.. cmd:: Extraction TestCompile @qualid ... @qualid.
+.. cmd:: Extraction TestCompile {+ @qualid }
 
    All the mentioned objects and all their dependencies are extracted
    to a temporary |OCaml| file, just as in ``Extraction "file"``. Then
@@ -104,9 +104,9 @@ Setting the target language
 The ability to fix target language is the first and more important
 of the extraction options. Default is ``OCaml``.
 
-.. cmd:: Extraction Language OCaml.
-.. cmd:: Extraction Language Haskell.
-.. cmd:: Extraction Language Scheme.
+.. cmd:: Extraction Language OCaml
+.. cmd:: Extraction Language Haskell
+.. cmd:: Extraction Language Scheme
 
 Inlining and optimizations
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -163,22 +163,22 @@ The type-preserving optimizations are controlled by the following |Coq| options:
    Those heuristics are not always perfect; if you want to disable
    this feature, turn this option off.
 
-.. cmd:: Extraction Inline @qualid ... @qualid.
+.. cmd:: Extraction Inline {+ @qualid }
 
    In addition to the automatic inline feature, the constants
    mentionned by this command will always be inlined during extraction.
 
-.. cmd:: Extraction NoInline @qualid ... @qualid.
+.. cmd:: Extraction NoInline {+ @qualid }
 
    Conversely, the constants mentionned by this command will
    never be inlined during extraction.
 
-.. cmd:: Print Extraction Inline. 
+.. cmd:: Print Extraction Inline
 
    Prints the current state of the table recording the custom inlinings 
    declared by the two previous commands. 
 
-.. cmd:: Reset Extraction Inline.
+.. cmd:: Reset Extraction Inline
 
    Empties the table recording the custom inlinings (see the
    previous commands).
@@ -213,7 +213,7 @@ code elimination performed during extraction, in a way which
 is independent but complementary to the main elimination
 principles of extraction (logical parts and types).
 
-.. cmd:: Extraction Implicit @qualid [ @ident ... @ident ].
+.. cmd:: Extraction Implicit @qualid [ {+ @ident } ]
 
    This experimental command allows declaring some arguments of
    `qualid` as implicit, i.e. useless in extracted code and hence to
@@ -253,12 +253,12 @@ a closed term, and of course the system cannot guess the program which
 realizes an axiom.  Therefore, it is possible to tell the system
 what ML term corresponds to a given axiom. 
 
-.. cmd:: Extract Constant @qualid => @string.
+.. cmd:: Extract Constant @qualid => @string
 
    Give an ML extraction for the given constant.
    The `string` may be an identifier or a quoted string.
 
-.. cmd:: Extract Inlined Constant @qualid => @string.
+.. cmd:: Extract Inlined Constant @qualid => @string
 
    Same as the previous one, except that the given ML terms will
    be inlined everywhere instead of being declared via a ``let``.
@@ -285,7 +285,7 @@ Notice that in the case of type scheme axiom (i.e. whose type is an
 arity, that is a sequence of product finished by a sort), then some type
 variables have to be given (as quoted strings). The syntax is then:
 
-.. cmdv:: Extract Constant @qualid @string ... @string => @string.
+.. cmdv:: Extract Constant @qualid @string ... @string => @string
 
 The number of type variables is checked by the system. For example:
 
@@ -314,7 +314,7 @@ The system also provides a mechanism to specify ML terms for inductive
 types and constructors. For instance, the user may want to use the ML
 native boolean type instead of |Coq| one. The syntax is the following:
 
-.. cmd:: Extract Inductive @qualid => @string [ @string ... @string ].
+.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ]
 
    Give an ML extraction for the given inductive type. You must specify
    extractions for the type itself (first `string`) and all its
@@ -322,7 +322,7 @@ native boolean type instead of |Coq| one. The syntax is the following:
    the ML extraction must be an ML inductive datatype, and the native
    pattern-matching of the language will be used.
 
-.. cmdv:: Extract Inductive @qualid => @string [ @string ... @string ] @string.
+.. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string
 
    Same as before, with a final extra `string` that indicates how to
    perform pattern-matching over this inductive type. In this form,
@@ -396,16 +396,16 @@ code that is meant to be linked with the extracted code.
 For instance the module ``List`` exists both in |Coq| and in |OCaml|.
 It is possible to instruct the extraction not to use particular filenames.
 
-.. cmd:: Extraction Blacklist @ident ... @ident.
+.. cmd:: Extraction Blacklist {+ @ident }
 
    Instruct the extraction to avoid using these names as filenames
    for extracted code.
 
-.. cmd:: Print Extraction Blacklist.
+.. cmd:: Print Extraction Blacklist
 
    Show the current list of filenames the extraction should avoid.
 
-.. cmd:: Reset Extraction Blacklist.
+.. cmd:: Reset Extraction Blacklist
 
    Allow the extraction to use any filename.
 
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index c4c39f410..f5237e4fb 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -179,7 +179,7 @@ A parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm )`,
 :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)` can be
 declared with the following command:
 
-.. cmd::  Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m ) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident.
+.. cmd::  Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m ) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident
 
 after having required the ``Setoid`` module with the ``Require Setoid``
 command.
@@ -226,7 +226,7 @@ replace terms with related ones only in contexts that are syntactic
 compositions of parametric morphism instances declared with the
 following command.
 
-.. cmd:: Add Parametric Morphism (x1 : T1 ) ... (xk : Tk ) : (f t1 ... tn ) with signature sig as @ident.
+.. cmd:: Add Parametric Morphism (x1 : T1 ) ... (xk : Tk ) : (f t1 ... tn ) with signature sig as @ident
 
 The command declares ``f`` as a parametric morphism of signature ``sig``. The
 identifier ``id`` gives a unique name to the morphism and it is used as
@@ -598,7 +598,7 @@ packing together the reflexivity, symmetry and transitivity lemmas).
 Notice that the syntax is not completely backward compatible since the
 identifier was not required.
 
-.. cmd:: Add Morphism f : @ident.
+.. cmd:: Add Morphism f : @ident
 
 The latter command also is restricted to the declaration of morphisms
 without parameters. It is not fully backward compatible since the
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 3f4ef2232..5f8c06484 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -124,7 +124,7 @@ term consists of the successive application of its coercions.
 Declaration of Coercions
 -------------------------
 
-.. cmd:: Coercion @qualid : @class >-> @class.
+.. cmd:: Coercion @qualid : @class >-> @class
 
   Declares the construction denoted by `qualid` as a coercion between
   the two given classes.
@@ -144,22 +144,22 @@ Declaration of Coercions
     valid coercion paths are ignored; they are signaled by a warning
     displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
 
-  .. cmdv:: Local Coercion @qualid : @class >-> @class.
+  .. cmdv:: Local Coercion @qualid : @class >-> @class
 
     Declares the construction denoted by `qualid` as a coercion local to
     the current section.
 
-  .. cmdv:: Coercion @ident := @term.
+  .. cmdv:: Coercion @ident := @term
 
     This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
     and then declares `ident` as a coercion between it source and its target.
 
-  .. cmdv:: Coercion @ident := @term : @type.
+  .. cmdv:: Coercion @ident := @term : @type
 
     This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
     and then declares `ident` as a coercion between it source and its target.
 
-  .. cmdv:: Local Coercion @ident := @term.
+  .. cmdv:: Local Coercion @ident := @term
 
     This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
     and then declares `ident` as a coercion between it source and its target.
@@ -202,7 +202,7 @@ grammar of inductive types from Figure :ref:`vernacular` as follows:
 Especially, if the extra ``>`` is present in a constructor
 declaration, this constructor is declared as a coercion.
 
-.. cmd:: Identity Coercion @ident : @class >-> @class.
+.. cmd:: Identity Coercion @ident : @class >-> @class
 
   If ``C`` is the source `class` and ``D`` the destination, we check
   that ``C`` is a constant with a body of the form
@@ -213,11 +213,11 @@ declaration, this constructor is declared as a coercion.
 
   .. exn:: @class must be a transparent constant.
 
-  .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident.
+  .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident
 
     Idem but locally to the current section.
 
-  .. cmdv:: SubClass @ident := @type.
+  .. cmdv:: SubClass @ident := @type
      :name: SubClass
 
     If `type` is a class `ident'` applied to some arguments then
@@ -229,7 +229,7 @@ declaration, this constructor is declared as a coercion.
 
       ``Identity Coercion`` `Id_ident_ident'` : `ident` ``>->`` `ident'`.
 
-  .. cmdv:: Local SubClass @ident := @type.
+  .. cmdv:: Local SubClass @ident := @type
 
     Same as before but locally to the current section.
 
@@ -237,19 +237,19 @@ declaration, this constructor is declared as a coercion.
 Displaying Available Coercions
 -------------------------------
 
-.. cmd:: Print Classes.
+.. cmd:: Print Classes
 
   Print the list of declared classes in the current context.
 
-.. cmd:: Print Coercions.
+.. cmd:: Print Coercions
 
   Print the list of declared coercions in the current context.
 
-.. cmd:: Print Graph.
+.. cmd:: Print Graph
 
   Print the list of valid coercion paths in the current context.
 
-.. cmd:: Print Coercion Paths @class @class.
+.. cmd:: Print Coercion Paths @class @class
 
   Print the list of valid coercion paths between the two given classes.
 
@@ -275,7 +275,7 @@ Classes as Records
 We allow the definition of *Structures with Inheritance* (or classes as records)
 by extending the existing :cmd:`Record` macro. Its new syntax is:
 
-.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }.
+.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }
 
    The first identifier `ident` is the name of the defined record and
    `sort` is its type. The optional identifier after ``:=`` is the name
@@ -291,7 +291,7 @@ by extending the existing :cmd:`Record` macro. Its new syntax is:
    (this may fail if the uniform inheritance condition is not
    satisfied).
 
-.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }.
+.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }
    :name: Structure
 
    This is a synonym of :cmd:`Record`.
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index 3ac7361c7..b685e68e4 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -145,7 +145,7 @@ prove some goals to construct the final definitions.
 Program Definition
 ~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Definition @ident := @term.
+.. cmd:: Program Definition @ident := @term
 
    This command types the value term in Russell and generates proof
    obligations. Once solved using the commands shown below, it binds the
@@ -167,7 +167,7 @@ Program Definition
       .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ...
 
 
-   .. cmdv:: Program Definition @ident @binders : @type := @term.
+   .. cmdv:: Program Definition @ident @binders : @type := @term
 
       This is equivalent to:
 
@@ -182,7 +182,7 @@ See also: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`un
 Program Fixpoint
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term.
+.. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term
 
 The optional order annotation follows the grammar:
 
@@ -255,7 +255,7 @@ using the syntax:
 Program Lemma
 ~~~~~~~~~~~~~
 
-.. cmd:: Program Lemma @ident : @type.
+.. cmd:: Program Lemma @ident : @type
 
    The Russell language can also be used to type statements of logical
    properties. It will generate obligations, try to solve them
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 11308e7e7..47d3a7d7c 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -303,7 +303,7 @@ following property:
 
 The syntax for adding a new ring is 
 
-.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}.
+.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )}
 
 The :n:`@ident` is not relevant. It is just used for error messages. The
 :n:`@term` is a proof that the ring signature satisfies the (semi-)ring
@@ -656,7 +656,7 @@ zero for the correctness of the algorithm.
 
 The syntax for adding a new field is 
 
-.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )}.
+.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )}
 
 The :n:`@ident` is not relevant. It is just used for error
 messages. :n:`@term` is a proof that the field signature satisfies the
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 3e95bd8c4..da9d3d7b6 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -272,7 +272,7 @@ Summary of the commands
 
 .. _Class:
 
-.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }.
+.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }
 
    The ``Class`` command is used to declare a type class with parameters
    ``binders`` and fields the declared record fields.
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index b8587d382..e80cfb6bb 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -367,7 +367,7 @@ Explicit Universes
 The syntax has been extended to allow users to explicitly bind names
 to universes and explicitly instantiate polymorphic definitions.
 
-.. cmd:: Universe @ident.
+.. cmd:: Universe @ident
 
    In the monorphic case, this command declares a new global universe
    named :g:`ident`, which can be referred to using its qualified name
@@ -378,7 +378,7 @@ to universes and explicitly instantiate polymorphic definitions.
    declarations in the same section.
 
 
-.. cmd:: Constraint @ident @ord @ident.
+.. cmd:: Constraint @ident @ord @ident
 
    This command declares a new constraint between named universes. The
    order relation :n:`@ord` can be one of :math:`<`, :math:`≤` or :math:`=`. If consistent, the constraint