Clean-up around cmd documentation.

In particular, remove trailing dots.

14 files changed, 309 insertions, 307 deletions

diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 1bac874518..cb93d48a41 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 c4c39f4104..f5237e4fbf 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 3f4ef22320..5f8c064840 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 3ac7361c77..b685e68e43 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 11308e7e76..47d3a7d7cd 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 3e95bd8c45..da9d3d7b6a 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 b8587d382d..e80cfb6bb5 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
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 8cafe84a05..8746897e75 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -30,7 +30,7 @@ expressions. In this sense, the ``Record`` construction allows defining
 
 In the expression:
 
-.. cmd:: Record @ident {* @param } {? : @sort} := {? @ident} { {*; @ident {* @binder } : @term } }.
+.. cmd:: Record @ident {* @param } {? : @sort} := {? @ident} { {*; @ident {* @binder } : @term } }
 
 the first identifier `ident` is the name of the defined record and `sort` is its
 type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted,
@@ -70,7 +70,7 @@ depends on both ``top`` and ``bottom``.
 Let us now see the work done by the ``Record`` macro. First the macro
 generates a variant type definition with just one constructor:
 
-.. cmd:: Variant @ident {* @params} : @sort := @ident {* (@ident : @term_1)}.
+.. cmd:: Variant @ident {* @params} : @sort := @ident {* (@ident : @term_1)}
 
 To build an object of type `ident`, one should provide the constructor
 |ident_0| with the appropriate number of terms filling the fields of the record.
@@ -105,15 +105,15 @@ to be all present if the missing ones can be inferred or prompted for
 
 This syntax can be disabled globally for printing by
 
-.. cmd:: Unset Printing Records.
+.. cmd:: Unset Printing Records
 
 For a given type, one can override this using either
 
-.. cmd:: Add Printing Record @ident.
+.. cmd:: Add Printing Record @ident
 
 to get record syntax or
 
-.. cmd:: Add Printing Constructor @ident.
+.. cmd:: Add Printing Constructor @ident
 
 to get constructor syntax.
 
@@ -539,23 +539,23 @@ Printing matching on irrefutable patterns
 If an inductive type has just one constructor, pattern-matching can be
 written using the first destructuring let syntax.
 
-.. cmd:: Add Printing Let @ident.
+.. cmd:: Add Printing Let @ident
 
    This adds `ident` to the list of inductive types for which pattern-matching
    is written using a let expression.
 
-.. cmd:: Remove Printing Let @ident.
+.. cmd:: Remove Printing Let @ident
 
    This removes ident from this list. Note that removing an inductive
    type from this list has an impact only for pattern-matching written
    using :g:`match`. Pattern-matching explicitly written using a destructuring
    :g:`let` are not impacted.
 
-.. cmd:: Test Printing Let for @ident.
+.. cmd:: Test Printing Let for @ident
 
    This tells if `ident` belongs to the list.
 
-.. cmd:: Print Table Printing Let.
+.. cmd:: Print Table Printing Let
 
    This prints the list of inductive types for which pattern-matching is
    written using a let expression.
@@ -571,20 +571,20 @@ Printing matching on booleans
 If an inductive type is isomorphic to the boolean type, pattern-matching
 can be written using ``if`` … ``then`` … ``else`` …:
 
-.. cmd:: Add Printing If @ident.
+.. cmd:: Add Printing If @ident
 
    This adds ident to the list of inductive types for which pattern-matching is
    written using an if expression.
 
-.. cmd:: Remove Printing If @ident.
+.. cmd:: Remove Printing If @ident
 
    This removes ident from this list.
 
-.. cmd:: Test Printing If for @ident.
+.. cmd:: Test Printing If for @ident
 
    This tells if ident belongs to the list.
 
-.. cmd:: Print Table Printing If.
+.. cmd:: Print Table Printing If
 
    This prints the list of inductive types for which pattern-matching is
    written using an if expression.
@@ -622,7 +622,7 @@ Advanced recursive functions
 
 The following experimental command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``:
 
-.. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term.
+.. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term
 
 This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper
 for several ways of defining a function *and other useful related
@@ -782,12 +782,12 @@ structured sections. Then local declarations become available (see
 Section :ref:`gallina-definitions`).
 
 
-.. cmd:: Section @ident.
+.. cmd:: Section @ident
 
    This command is used to open a section named `ident`.
 
 
-.. cmd:: End @ident.
+.. cmd:: End @ident
 
     This command closes the section named `ident`. After closing of the
     section, the local declarations (variables and local definitions) get
@@ -852,25 +852,25 @@ In the syntax of module application, the ! prefix indicates that any
 (see the ``Module Type`` command below).
 
 
-.. cmd:: Module @ident.
+.. cmd:: Module @ident
 
    This command is used to start an interactive module named `ident`.
 
-.. cmdv:: Module @ident {* @module_binding}.
+.. cmdv:: Module @ident {* @module_binding}
 
    Starts an interactive functor with
    parameters given by module_bindings.
 
-.. cmdv:: Module @ident : @module_type.
+.. cmdv:: Module @ident : @module_type
 
    Starts an interactive module specifying its module type.
 
-.. cmdv:: Module @ident {* @module_binding} : @module_type.
+.. cmdv:: Module @ident {* @module_binding} : @module_type
 
    Starts an interactive functor with parameters given by the list of `module binding`, and output module
    type `module_type`.
 
-.. cmdv:: Module @ident <: {+<: @module_type }.
+.. cmdv:: Module @ident <: {+<: @module_type }
 
    Starts an interactive module satisfying each `module_type`.
 
@@ -879,14 +879,14 @@ In the syntax of module application, the ! prefix indicates that any
    Starts an interactive functor with parameters given by the list of `module_binding`. The output module type
    is verified against each `module_type`.
 
-.. cmdv:: Module [ Import | Export ].
+.. cmdv:: Module [ Import | Export ]
 
    Behaves like ``Module``, but automatically imports or exports the module.
 
 Reserved commands inside an interactive module
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Include @module.
+.. cmd:: Include @module
 
    Includes the content of module in the current
    interactive module. Here module can be a module expression or a module
@@ -894,11 +894,11 @@ Reserved commands inside an interactive module
    expression then the system tries to instantiate module by the current
    interactive module.
 
-.. cmd:: Include {+<+ @module}.
+.. cmd:: Include {+<+ @module}
 
    is a shortcut for the commands ``Include`` `module` for each `module`.
 
-.. cmd:: End @ident.
+.. cmd:: End @ident
 
    This command closes the interactive module `ident`. If the module type
    was given the content of the module is matched against it and an error
@@ -912,34 +912,34 @@ Reserved commands inside an interactive module
 
     .. exn:: This is not the last opened module.
 
-.. cmd:: Module @ident := @module_expression.
+.. cmd:: Module @ident := @module_expression
 
     This command defines the module identifier `ident` to be equal
     to `module_expression`.
 
-    .. cmdv:: Module @ident {* @module_binding} := @module_expression.
+    .. cmdv:: Module @ident {* @module_binding} := @module_expression
 
        Defines a functor with parameters given by the list of `module_binding` and body `module_expression`.
 
-    .. cmdv:: Module @ident {* @module_binding} : @module_type := @module_expression.
+    .. cmdv:: Module @ident {* @module_binding} : @module_type := @module_expression
 
        Defines a functor with parameters given by the list of `module_binding` (possibly none), and output module type `module_type`,
        with body `module_expression`.
 
-    .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression.
+    .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression
 
        Defines a functor with parameters given by module_bindings (possibly none) with body `module_expression`.
        The body is checked against each |module_type_i|.
 
-    .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression}.
+    .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression}
 
        is equivalent to an interactive module where each `module_expression` is included.
 
-.. cmd:: Module Type @ident.
+.. cmd:: Module Type @ident
 
 This command is used to start an interactive module type `ident`.
 
-    .. cmdv:: Module Type @ident {* @module_binding}.
+    .. cmdv:: Module Type @ident {* @module_binding}
 
        Starts an interactive functor type with parameters given by `module_bindings`.
 
@@ -947,11 +947,11 @@ This command is used to start an interactive module type `ident`.
 Reserved commands inside an interactive module type:
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Include @module.
+.. cmd:: Include @module
 
    Same as ``Include`` inside a module.
 
-.. cmd:: Include {+<+ @module}.
+.. cmd:: Include {+<+ @module}
 
    is a shortcut for the command ``Include`` `module` for each `module`.
 
@@ -961,30 +961,30 @@ Reserved commands inside an interactive module type:
    The instance of this assumption will be automatically expanded at functor application, except when
    this functor application is prefixed by a ``!`` annotation.
 
-.. cmd:: End @ident.
+.. cmd:: End @ident
 
    This command closes the interactive module type `ident`.
 
    .. exn:: This is not the last opened module type.
 
-.. cmd:: Module Type @ident := @module_type.
+.. cmd:: Module Type @ident := @module_type
 
    Defines a module type `ident` equal to `module_type`.
 
-    .. cmdv:: Module Type @ident {* @module_binding} := @module_type.
+    .. cmdv:: Module Type @ident {* @module_binding} := @module_type
 
        Defines a functor type `ident` specifying functors taking arguments `module_bindings` and
        returning `module_type`.
 
-    .. cmdv:: Module Type @ident {* @module_binding} := {+<+ @module_type }.
+    .. cmdv:: Module Type @ident {* @module_binding} := {+<+ @module_type }
 
        is equivalent to an interactive module type were each `module_type` is included.
 
-.. cmd:: Declare Module @ident : @module_type.
+.. cmd:: Declare Module @ident : @module_type
 
    Declares a module `ident` of type `module_type`.
 
-    .. cmdv:: Declare Module @ident {* @module_binding} : @module_type.
+    .. cmdv:: Declare Module @ident {* @module_binding} : @module_type
 
        Declares a functor with parameters given by the list of `module_binding` and output module type
        `module_type`.
@@ -1170,7 +1170,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified.
 
 .. _import_qualid:
 
-.. cmd:: Import @qualid.
+.. cmd:: Import @qualid
 
     If `qualid` denotes a valid basic module (i.e. its module type is a
     signature), makes its components available by their short names.
@@ -1229,11 +1229,11 @@ qualified name.
 
     .. warn:: Trying to mask the absolute name @qualid!
 
-.. cmd:: Print Module @ident.
+.. cmd:: Print Module @ident
 
     Prints the module type and (optionally) the body of the module `ident`.
 
-.. cmd:: Print Module Type @ident.
+.. cmd:: Print Module Type @ident
 
     Prints the module type corresponding to `ident`.
 
@@ -1588,7 +1588,7 @@ Declaring Implicit Arguments
 
 To set implicit arguments *a posteriori*, one can use the command:
 
-.. cmd:: Arguments @qualid {* @possibly_bracketed_ident }.
+.. cmd:: Arguments @qualid {* @possibly_bracketed_ident }
    :name: Arguments (implicits)
 
 where the list of `possibly_bracketed_ident` is a prefix of the list of
@@ -1602,7 +1602,7 @@ of `qualid`.
 
 Implicit arguments can be cleared with the following syntax:
 
-.. cmd:: Arguments @qualid : clear implicits.
+.. cmd:: Arguments @qualid : clear implicits
 
 .. cmdv:: Global Arguments @qualid {* @possibly_bracketed_ident }
 
@@ -1611,13 +1611,13 @@ Implicit arguments can be cleared with the following syntax:
    implicit arguments known from inside the section to be the ones
    declared by the command.
 
-.. cmdv:: Local Arguments @qualid {* @possibly_bracketed_ident }.
+.. cmdv:: Local Arguments @qualid {* @possibly_bracketed_ident }
 
    When in a module, tell not to activate the
    implicit arguments ofqualid declared by this command to contexts that
    require the module.
 
-.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ @possibly_bracketed_ident } }.
+.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ @possibly_bracketed_ident } }
 
    For names of constants, inductive types,
    constructors, lemmas which can only be applied to a fixed number of
@@ -1669,7 +1669,7 @@ Automatic declaration of implicit arguments
 |Coq| can also automatically detect what are the implicit arguments of a
 defined object. The command is just
 
-.. cmd:: Arguments @qualid : default implicits.
+.. cmd:: Arguments @qualid : default implicits
 
 The auto-detection is governed by options telling if strict,
 contextual, or reversible-pattern implicit arguments must be
@@ -1842,7 +1842,7 @@ Renaming implicit arguments
 
 Implicit arguments names can be redefined using the following syntax:
 
-.. cmd:: Arguments @qualid {* @name} : @rename.
+.. cmd:: Arguments @qualid {* @name} : @rename
 
 With the assert flag, ``Arguments`` can be used to assert that a given
 object has the expected number of arguments and that these arguments
@@ -1933,7 +1933,7 @@ Assume that `qualid` denotes an object ``(Build_struc`` |c_1| … |c_n| ``)`` in
 structure *struct* of which the fields are |x_1|, …, |x_n|. Assume that
 `qualid` is declared as a canonical structure using the command
 
-.. cmd:: Canonical Structure @qualid.
+.. cmd:: Canonical Structure @qualid
 
 Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
 solved during the type-checking process, `qualid` is used as a solution.
@@ -1974,11 +1974,11 @@ and ``B`` can be synthesized in the next statement.
 Remark: If a same field occurs in several canonical structure, then
 only the structure declared first as canonical is considered.
 
-.. cmdv:: Canonical Structure @ident := @term : @type.
+.. cmdv:: Canonical Structure @ident := @term : @type
 
-.. cmdv:: Canonical Structure @ident := @term.
+.. cmdv:: Canonical Structure @ident := @term
 
-.. cmdv:: Canonical Structure @ident : @type := @term.
+.. cmdv:: Canonical Structure @ident : @type := @term
 
 These are equivalent to a regular definition of `ident` followed by the declaration
 ``Canonical Structure`` `ident`.
@@ -2006,7 +2006,7 @@ It is possible to bind variable names to a given type (e.g. in a
 development using arithmetic, it may be convenient to bind the names `n`
 or `m` to the type ``nat`` of natural numbers). The command for that is
 
-.. cmd:: Implicit Types {+ @ident } : @type.
+.. cmd:: Implicit Types {+ @ident } : @type
 
 The effect of the command is to automatically set the type of bound
 variables starting with `ident` (either `ident` itself or `ident` followed by
@@ -2028,7 +2028,7 @@ case, this latter type is considered).
 
        Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m.
 
-.. cmdv:: Implicit Type @ident : @type.
+.. cmdv:: Implicit Type @ident : @type
 
   This is useful for declaring the implicit type of a single variable.
 
@@ -2067,7 +2067,7 @@ the ``Generalizable`` vernacular command to avoid unexpected
 generalizations when mistyping identifiers. There are several commands
 that specify which variables should be generalizable.
 
-.. cmd:: Generalizable All Variables.
+.. cmd:: Generalizable All Variables
 
    All variables are candidate for
    generalization if they appear free in the context under a
@@ -2075,16 +2075,16 @@ that specify which variables should be generalizable.
    of typos. In such cases, the context will probably contain some
    unexpected generalized variable.
 
-.. cmd:: Generalizable No Variables.
+.. cmd:: Generalizable No Variables
 
    Disable implicit generalization  entirely. This is the default behavior.
 
-.. cmd:: Generalizable (Variable | Variables) {+ @ident }.
+.. cmd:: Generalizable (Variable | Variables) {+ @ident }
 
    Allow generalization of the given identifiers only. Calling this command multiple times
    adds to the allowed identifiers.
 
-.. cmd:: Global Generalizable.
+.. cmd:: Global Generalizable
 
    Allows exporting the choice of generalizable variables.
 
@@ -2159,7 +2159,7 @@ Constructions.
 The constraints on the internal level of the occurrences of Type
 (see :ref:`Sorts`) can be printed using the command
 
-.. cmd:: Print {? Sorted} Universes.
+.. cmd:: Print {? Sorted} Universes
    :name: Print Universes
 
 If the optional ``Sorted`` option is given, each universe will be made
@@ -2168,7 +2168,7 @@ ordering) in the universe hierarchy.
 
 This command also accepts an optional output filename:
 
-.. cmdv:: Print {? Sorted} Universes @string.
+.. cmdv:: Print {? Sorted} Universes @string
 
 If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
 language, and can be processed by Graphviz tools. The format is
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 44bf255bb8..46e684b122 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -551,7 +551,7 @@ has type :token:`type`.
 
 .. _Axiom:
 
-.. cmd:: Axiom @ident : @term.
+.. cmd:: Axiom @ident : @term
 
    This command links *term* to the name *ident* as its specification in
    the global context. The fact asserted by *term* is thus assumed as a
@@ -560,24 +560,24 @@ has type :token:`type`.
 .. exn:: @ident already exists.
    :name: @ident already exists. (Axiom)
 
-.. cmdv:: Parameter @ident : @term.
+.. cmdv:: Parameter @ident : @term
    :name: Parameter
 
    Is equivalent to ``Axiom`` :token:`ident` : :token:`term`
 
-.. cmdv:: Parameter {+ @ident } : @term.
+.. cmdv:: Parameter {+ @ident } : @term
 
    Adds parameters with specification :token:`term`
 
-.. cmdv:: Parameter {+ ( {+ @ident } : @term ) }.
+.. cmdv:: Parameter {+ ( {+ @ident } : @term ) }
 
    Adds blocks of parameters with different specifications.
 
-.. cmdv:: Parameters {+ ( {+ @ident } : @term ) }.
+.. cmdv:: Parameters {+ ( {+ @ident } : @term ) }
 
    Synonym of ``Parameter``.
 
-.. cmdv:: Local Axiom @ident : @term.
+.. cmdv:: Local Axiom @ident : @term
 
    Such axioms are never made accessible through their unqualified name by
    :cmd:`Import` and its variants. You have to explicitly give their fully
@@ -588,7 +588,7 @@ has type :token:`type`.
 
    Is equivalent to ``Axiom`` :token:`ident` : :token:`term`.
 
-.. cmd:: Variable @ident : @term.
+.. cmd:: Variable @ident : @term
 
 This command links :token:`term` to the name :token:`ident` in the context of
 the current section (see Section :ref:`section-mechanism` for a description of
@@ -600,20 +600,20 @@ of any section is equivalent to using ``Local Parameter``.
 .. exn:: @ident already exists.
    :name: @ident already exists. (Variable)
 
-.. cmdv:: Variable {+ @ident } : @term.
+.. cmdv:: Variable {+ @ident } : @term
 
    Links :token:`term` to each :token:`ident`.
 
-.. cmdv:: Variable {+ ( {+ @ident } : @term) }.
+.. cmdv:: Variable {+ ( {+ @ident } : @term) }
 
    Adds blocks of variables with different specifications.
 
-.. cmdv:: Variables {+ ( {+ @ident } : @term) }.
+.. cmdv:: Variables {+ ( {+ @ident } : @term) }
 
-.. cmdv:: Hypothesis {+ ( {+ @ident } : @term) }.
+.. cmdv:: Hypothesis {+ ( {+ @ident } : @term) }
    :name: Hypothesis
 
-.. cmdv:: Hypotheses {+ ( {+ @ident } : @term) }.
+.. cmdv:: Hypotheses {+ ( {+ @ident } : @term) }
 
 Synonyms of ``Variable``.
 
@@ -643,7 +643,7 @@ type which is the type of its body.
 A formal presentation of constants and environments is given in
 Section :ref:`typing-rules`.
 
-.. cmd:: Definition @ident := @term.
+.. cmd:: Definition @ident := @term
 
    This command binds :token:`term` to the name :token:`ident` in the environment,
    provided that :token:`term` is well-typed.
@@ -651,31 +651,31 @@ Section :ref:`typing-rules`.
 .. exn:: @ident already exists.
    :name: @ident already exists. (Definition)
 
-.. cmdv:: Definition @ident : @term := @term.
+.. cmdv:: Definition @ident : @term := @term
 
    It checks that the type of :token:`term`:math:`_2` is definitionally equal to
    :token:`term`:math:`_1`, and registers :token:`ident` as being of type
    :token:`term`:math:`_1`, and bound to value :token:`term`:math:`_2`.
 
 
-.. cmdv:: Definition @ident {* @binder } : @term := @term.
+.. cmdv:: Definition @ident {* @binder } : @term := @term
 
    This is equivalent to ``Definition`` :token:`ident` : :g:`forall`
    :token:`binder`:math:`_1` … :token:`binder`:math:`_n`, :token:`term`:math:`_1` := 
    fun :token:`binder`:math:`_1` …
    :token:`binder`:math:`_n` => :token:`term`:math:`_2`.
 
-.. cmdv:: Local Definition @ident := @term.
+.. cmdv:: Local Definition @ident := @term
 
    Such definitions are never made accessible through their
    unqualified name by :cmd:`Import` and its variants.
    You have to explicitly give their fully qualified name to refer to them.
 
-.. cmdv:: Example @ident := @term.
+.. cmdv:: Example @ident := @term
 
-.. cmdv:: Example @ident : @term := @term.
+.. cmdv:: Example @ident : @term := @term
 
-.. cmdv:: Example @ident {* @binder } : @term := @term.
+.. cmdv:: Example @ident {* @binder } : @term := @term
 
 These are synonyms of the Definition forms.
 
@@ -683,7 +683,7 @@ These are synonyms of the Definition forms.
 
 See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
 
-.. cmd:: Let @ident := @term.
+.. cmd:: Let @ident := @term
 
 This command binds the value :token:`term` to the name :token:`ident` in the
 environment of the current section. The name :token:`ident` disappears when the
@@ -696,11 +696,11 @@ prefixed by the let-in definition ``let`` :token:`ident` ``:=`` :token:`term`
 .. exn:: @ident already exists.
    :name: @ident already exists. (Let)
 
-.. cmdv:: Let @ident : @term := @term.
+.. cmdv:: Let @ident : @term := @term
 
-.. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body}.
+.. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body}
 
-.. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}.
+.. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}
 
 See also Sections :ref:`section-mechanism`, commands :cmd:`Opaque`,
 :cmd:`Transparent`, and tactic :tacn:`unfold`.
@@ -916,7 +916,7 @@ Mutually defined inductive types
 
 The definition of a block of mutually inductive types has the form:
 
-.. cmdv:: Inductive @ident : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident : @term := {? | } @ident : @type {* | @ident : @type }}.
+.. cmdv:: Inductive @ident : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident : @term := {? | } @ident : @type {* | @ident : @type }}
 
 It has the same semantics as the above ``Inductive`` definition for each
 :token:`ident` All :token:`ident` are simultaneously added to the environment.
@@ -928,7 +928,7 @@ parameters correspond to a local context in which the whole set of
 inductive declarations is done. For this reason, the parameters must be
 strictly the same for each inductive types The extended syntax is:
 
-.. cmdv:: Inductive @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type }}.
+.. cmdv:: Inductive @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type }}
 
 The typical example of a mutual inductive data type is the one for trees and
 forests. We assume given two types :g:`A` and :g:`B` as variables. It can
@@ -1041,7 +1041,7 @@ constructions.
 
 .. _Fixpoint:
 
-.. cmd:: Fixpoint @ident @params {struct @ident} : @type := @term.
+.. cmd:: Fixpoint @ident @params {struct @ident} : @type := @term
 
 This command allows defining functions by pattern-matching over inductive objects
 using a fixed point construction. The meaning of this declaration is to
@@ -1155,7 +1155,7 @@ The ``Fixpoint`` construction enjoys also the with extension to define functions
 over mutually defined inductive types or more generally any mutually recursive
 definitions.
 
-.. cmdv:: Fixpoint @ident @params {struct @ident} : @type := @term {* with @ident {+ @params} : @type := @term}.
+.. cmdv:: Fixpoint @ident @params {struct @ident} : @type := @term {* with @ident {+ @params} : @type := @term}
 
 allows to define simultaneously fixpoints.
 
@@ -1182,7 +1182,7 @@ induction principles. It is described in Section
 Definitions of recursive objects in co-inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: CoFixpoint @ident : @type := @term.
+.. cmd:: CoFixpoint @ident : @type := @term
 
 introduces a method for constructing an infinite object of a coinductive
 type. For example, the stream containing all natural numbers can be
@@ -1243,7 +1243,7 @@ inhabitant of the type) is interactively built using tactics. The interactive
 proof mode is described in Chapter :ref:`proofhandling` and the tactics in
 Chapter :ref:`Tactics`. The basic assertion command is:
 
-.. cmd:: Theorem @ident : @type.
+.. cmd:: Theorem @ident : @type
 
 After the statement is asserted, Coq needs a proof. Once a proof of
 :token:`type` under the assumptions represented by :token:`binders` is given and
@@ -1258,24 +1258,24 @@ the theorem is bound to the name :token:`ident` in the environment.
    The name you provided is already defined. You have then to choose
    another name.
 
-.. cmdv:: Lemma @ident : @type.
+.. cmdv:: Lemma @ident : @type
    :name: Lemma
 
-.. cmdv:: Remark @ident : @type.
+.. cmdv:: Remark @ident : @type
    :name: Remark
 
-.. cmdv:: Fact @ident : @type.
+.. cmdv:: Fact @ident : @type
    :name: Fact
 
-.. cmdv:: Corollary @ident : @type.
+.. cmdv:: Corollary @ident : @type
    :name: Corollary
 
-.. cmdv:: Proposition @ident : @type.
+.. cmdv:: Proposition @ident : @type
    :name: Proposition
 
    These commands are synonyms of ``Theorem`` :token:`ident` : :token:`type`.
 
-.. cmdv:: Theorem @ident : @type {* with @ident : @type}.
+.. cmdv:: Theorem @ident : @type {* with @ident : @type}
 
    This command is useful for theorems that are proved by simultaneous induction
    over a mutually inductive assumption, or that assert mutually dependent
@@ -1297,7 +1297,7 @@ the theorem is bound to the name :token:`ident` in the environment.
    The command can be used also with :cmd:`Lemma`, :cmd:`Remark`, etc. instead of
    :cmd:`Theorem`.
 
-.. cmdv:: Definition @ident : @type.
+.. cmdv:: Definition @ident : @type
 
    This allows defining a term of type :token:`type` using the proof editing
    mode. It behaves as Theorem but is intended to be used in conjunction with
@@ -1308,20 +1308,20 @@ the theorem is bound to the name :token:`ident` in the environment.
 
    See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
 
-.. cmdv:: Let @ident : @type.
+.. cmdv:: Let @ident : @type
 
    Like Definition :token:`ident` : :token:`type`. except that the definition is
    turned into a let-in definition generalized over the declarations depending
    on it after closing the current section.
 
-.. cmdv:: Fixpoint @ident @binders with .
+.. cmdv:: Fixpoint @ident @binders with
 
    This generalizes the syntax of Fixpoint so that one or more bodies
    can be defined interactively using the proof editing mode (when a
    body is omitted, its type is mandatory in the syntax). When the block
    of proofs is completed, it is intended to be ended by Defined.
 
-.. cmdv:: CoFixpoint @ident with.
+.. cmdv:: CoFixpoint @ident with
 
    This generalizes the syntax of CoFixpoint so that one or more bodies
    can be defined interactively using the proof editing mode.
@@ -1367,7 +1367,7 @@ the theorem is bound to the name :token:`ident` in the environment.
    unfolded in conversion tactics (see :ref:`performingcomputations`,
    :cmd:`Opaque`, :cmd:`Transparent`).
 
-.. cmdv:: Admitted.
+.. cmdv:: Admitted
    :name: Admitted
 
    Turns the current asserted statement into an axiom and exits the proof mode.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index dc9add66f9..d81048f075 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1092,7 +1092,7 @@ Basically, |Ltac| toplevel definitions are made as follows:
 Printing |Ltac| tactics
 ~~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Print Ltac @qualid.
+.. cmd:: Print Ltac @qualid
 
    Defined |Ltac| functions can be displayed using this command.
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 8643742ae0..9ee1c4eda5 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -49,7 +49,7 @@ the assertion of a theorem using an assertion command like :cmd:`Theorem`. The
 list of assertion commands is given in Section :ref:`Assertions`. The command
 :cmd:`Goal` can also be used.
 
-.. cmd:: Goal @form.
+.. cmd:: Goal @form
 
 This is intended for quick assertion of statements, without knowing in
 advance which name to give to the assertion, typically for quick
@@ -81,34 +81,36 @@ proof term is completely rechecked at this point, one may have to wait
 a while when the proof is large. In some exceptional cases one may
 even incur a memory overflow.
 
-.. cmdv:: Defined.
+.. cmdv:: Defined
    :name: Defined (interactive proof)
 
 Defines the proved term as a transparent constant.
 
-.. cmdv:: Save @ident.
+.. cmdv:: Save @ident
 
 Forces the name of the original goal to be :n:`@ident`. This
 command (and the following ones) can only be used if the original goal
 has been opened using the ``Goal`` command.
 
-.. cmd:: Admitted.
+.. cmd:: Admitted
    :name: Admitted (interactive proof)
 
 This command is available in interactive editing mode to give up
 the current proof and declare the initial goal as an axiom.
 
-.. cmd:: Proof @term.
+.. cmd:: Proof @term
    :name: Proof `term`
 
 This command applies in proof editing mode. It is equivalent to
 
-.. cmd:: exact @term. Qed.
+.. coqtop:: in
+
+   exact @term. Qed.
 
 That is, you have to give the full proof in one gulp, as a
 proof term (see Section :ref:`applyingtheorems`).
 
-.. cmdv:: Proof.
+.. cmdv:: Proof
    :name: Proof (interactive proof)
 
 Is a noop which is useful to delimit the sequence of tactic commands
@@ -121,7 +123,7 @@ See also: ``Proof with tactic.`` in Section
 :ref:`tactics-implicit-automation`.
 
 
-.. cmd:: Proof using @ident1 ... @identn.
+.. cmd:: Proof using @ident1 ... @identn
 
 This command applies in proof editing mode. It declares the set of
 section variables (see :ref:`gallina-assumptions`) used by the proof. At ``Qed`` time, the
@@ -133,23 +135,23 @@ example if ``T`` is variable and a is a variable of type ``T``, the commands
 ``Proof using a`` and ``Proof using T a``` are actually equivalent.
 
 
-.. cmdv:: Proof using @ident1 ... @identn with @tactic.
+.. cmdv:: Proof using @ident1 ... @identn with @tactic
 
 in Section :ref:`tactics-implicit-automation`.
 
-.. cmdv:: Proof using All.
+.. cmdv:: Proof using All
 
 Use all section variables.
 
 
-.. cmdv:: Proof using Type.
+.. cmdv:: Proof using Type
 
-.. cmdv:: Proof using.
+.. cmdv:: Proof using
 
 Use only section variables occurring in the statement.
 
 
-.. cmdv:: Proof using Type*.
+.. cmdv:: Proof using Type*
 
 The ``*`` operator computes the forward transitive closure. E.g. if the
 variable ``H`` has type ``p < 5`` then ``H`` is in ``p*`` since ``p`` occurs in the type
@@ -157,21 +159,21 @@ of ``H``. ``Type*`` is the forward transitive closure of the entire set of
 section variables occurring in the statement.
 
 
-.. cmdv:: Proof using -(@ident1 ... @identn).
+.. cmdv:: Proof using -(@ident1 ... @identn)
 
 Use all section variables except :n:`@ident1` ... :n:`@identn`.
 
 
-.. cmdv:: Proof using @collection1 + @collection2 .
+.. cmdv:: Proof using @collection1 + @collection2
 
 
-.. cmdv:: Proof using @collection1 - @collection2 .
+.. cmdv:: Proof using @collection1 - @collection2
 
 
-.. cmdv:: Proof using @collection - ( @ident1 ... @identn ).
+.. cmdv:: Proof using @collection - ( @ident1 ... @identn )
 
 
-.. cmdv:: Proof using @collection * .
+.. cmdv:: Proof using @collection *
 
 Use section variables being, respectively, in the set union, set
 difference, set complement, set forward transitive closure. See
@@ -232,7 +234,7 @@ Define the collection named "Many" containing the set difference of
 "Fewer" and the unnamed collection ``x`` ``y``
 
 
-.. cmd:: Abort.
+.. cmd:: Abort
 
 This command cancels the current proof development, switching back to
 the previous proof development, or to the |Coq| toplevel if no other
@@ -243,18 +245,18 @@ proof was edited.
 
 
 
-.. cmdv::  Abort @ident.
+.. cmdv::  Abort @ident
 
 Aborts the editing of the proof named :n:`@ident`.
 
-.. cmdv:: Abort All.
+.. cmdv:: Abort All
 
 Aborts all current goals, switching back to the |Coq|
 toplevel.
 
 
 
-.. cmd:: Existential @num := @term.
+.. cmd:: Existential @num := @term
 
 This command instantiates an existential variable. :n:`@num` is an index in
 the list of uninstantiated existential variables displayed by ``Show
@@ -271,7 +273,7 @@ See also: ``instantiate (num:= term).`` in Section
 See also: ``Grab Existential Variables.`` below.
 
 
-.. cmd:: Grab Existential Variables.
+.. cmd:: Grab Existential Variables
 
 This command can be run when a proof has no more goal to be solved but
 has remaining uninstantiated existential variables. It takes every
@@ -282,17 +284,17 @@ Navigation in the proof tree
 --------------------------------
 
 
-.. cmd:: Undo.
+.. cmd:: Undo
 
 This command cancels the effect of the last command. Thus, it
 backtracks one step.
 
 
-.. cmdv:: Undo @num.
+.. cmdv:: Undo @num
 
 Repeats Undo :n:`@num` times.
 
-.. cmdv:: Restart.
+.. cmdv:: Restart
    :name: Restart
 
 This command restores the proof editing process to the original goal.
@@ -301,7 +303,7 @@ This command restores the proof editing process to the original goal.
 .. exn:: No focused proof to restart.
 
 
-.. cmd:: Focus.
+.. cmd:: Focus
 
 This focuses the attention on the first subgoal to prove and the
 printing of the other subgoals is suspended until the focused subgoal
@@ -309,7 +311,7 @@ is solved or unfocused. This is useful when there are many current
 subgoals which clutter your screen.
 
 
-.. cmdv:: Focus @num.
+.. cmdv:: Focus @num
 
 This focuses the attention on the :n:`@num` th subgoal to
 prove.
@@ -317,14 +319,14 @@ prove.
 *This command is deprecated since 8.8*: prefer the use of bullets or
 focusing brackets instead, including :n:`@num : %{`
 
-.. cmd:: Unfocus.
+.. cmd:: Unfocus
 
 This command restores to focus the goal that were suspended by the
 last ``Focus`` command.
 
 *This command is deprecated since 8.8.*
 
-.. cmd:: Unfocused.
+.. cmd:: Unfocused
 
 Succeeds if the proof is fully unfocused, fails if there are some
 goals out of focus.
@@ -440,7 +442,7 @@ Requesting information
 ----------------------
 
 
-.. cmd:: Show.
+.. cmd:: Show
 
 This command displays the current goals.
 
@@ -452,7 +454,7 @@ Displays only the :n:`@num`-th subgoal.
 .. exn:: No such goal.
 .. exn:: No focused proof.
 
-.. cmdv:: Show @ident.
+.. cmdv:: Show @ident
 
 Displays the named goal :n:`@ident`. This is useful in
 particular to display a shelved goal but only works if the
@@ -467,7 +469,7 @@ corresponding existential variable has been named by the user
     eexists ?[n].
     Show n.
 
-.. cmdv:: Show Script.
+.. cmdv:: Show Script
 
 Displays the whole list of tactics applied from the
 beginning of the current proof. This tactics script may contain some
@@ -475,7 +477,7 @@ holes (subgoals not yet proved). They are printed under the form
 
 ``<Your Tactic Text here>``.
 
-.. cmdv:: Show Proof.
+.. cmdv:: Show Proof
 
 It displays the proof term generated by the tactics
 that have been applied. If the proof is not completed, this term
@@ -485,14 +487,14 @@ integer, and applied to the list of variables in the context, since it
 may depend on them. The types obtained by abstracting away the context
 from the type of each hole-placer are also printed.
 
-.. cmdv:: Show Conjectures.
+.. cmdv:: Show Conjectures
 
 It prints the list of the names of all the
 theorems that are currently being proved. As it is possible to start
 proving a previous lemma during the proof of a theorem, this list may
 contain several names.
 
-.. cmdv:: Show Intro.
+.. cmdv:: Show Intro
 
 If the current goal begins by at least one product,
 this command prints the name of the first product, as it would be
@@ -502,18 +504,18 @@ Proof General macro, it is possible to transform any anonymous ``intro``
 into a qualified one such as ``intro y13``. In the case of a non-product
 goal, it prints nothing.
 
-.. cmdv:: Show Intros.
+.. cmdv:: Show Intros
 
 This command is similar to the previous one, it
 simulates the naming process of an intros.
 
-.. cmdv:: Show Existentials.
+.. cmdv:: Show Existentials
 
 It displays the set of all uninstantiated
 existential variables in the current proof tree, along with the type
 and the context of each variable.
 
-.. cmdv:: Show Match @ident.
+.. cmdv:: Show Match @ident
 
 This variant displays a template of the Gallina
 ``match`` construct with a branch for each constructor of the type
@@ -528,14 +530,14 @@ This variant displays a template of the Gallina
 
 .. _ShowUniverses:
 
-.. cmdv:: Show Universes.
+.. cmdv:: Show Universes
 
 It displays the set of all universe constraints and
 its normalized form at the current stage of the proof, useful for
 debugging universe inconsistencies.
 
 
-.. cmd:: Guarded.
+.. cmd:: Guarded
 
 Some tactics (e.g. :tacn:`refine`) allow to build proofs using
 fixpoint or co-fixpoint constructions. Due to the incremental nature
@@ -580,13 +582,13 @@ When experiencing high memory usage the following commands can be used
 to force |Coq| to optimize some of its internal data structures.
 
 
-.. cmd:: Optimize Proof.
+.. cmd:: Optimize Proof
 
 This command forces |Coq| to shrink the data structure used to represent
 the ongoing proof.
 
 
-.. cmd:: Optimize Heap.
+.. cmd:: Optimize Heap
 
 This command forces the |OCaml| runtime to perform a heap compaction.
 This is in general an expensive operation.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 8816c934a6..63cd0f3ead 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -423,7 +423,7 @@ an improvement over ``all null s``.
 
 The syntax of the new declaration is
 
-.. cmd:: Prenex Implicits {+ @ident}.
+.. cmd:: Prenex Implicits {+ @ident}
 
 Let us denote :math:`c_1` … :math:`c_n` the list of identifiers given to a
 ``Prenex Implicits`` command.  The command checks that each ci is the name of
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index dff3c53bc0..8f4cbaf35c 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3307,7 +3307,7 @@ One can optionally declare a hint database using the command ``Create
 HintDb``. If a hint is added to an unknown database, it will be
 automatically created.
 
-.. cmd:: Create HintDb @ident {? discriminated}.
+.. cmd:: Create HintDb @ident {? discriminated}
 
 This command creates a new database named :n:`@ident`. The database is
 implemented by a Discrimination Tree (DT) that serves as an index of
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index ca80da60ae..838310819b 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -14,7 +14,7 @@ Displaying
 
 .. _Print:
 
-.. cmd:: Print @qualid.
+.. cmd:: Print @qualid
    :name: Print
 
 This command displays on the screen information about the declared or
@@ -34,13 +34,13 @@ Error messages:
 Variants:
 
 
-.. cmdv:: Print Term @qualid.
+.. cmdv:: Print Term @qualid
    :name: Print Term
 
 This is a synonym of :cmd:`Print` :n:`@qualid` when :n:`@qualid`
 denotes a global constant.
 
-.. cmdv:: About @qualid.
+.. cmdv:: About @qualid
    :name: About
 
 This displays various information about the object
@@ -54,7 +54,7 @@ This locally renames the polymorphic universes of :n:`@qualid`.
 An underscore means the raw universe is printed.
 This form can be used with :cmd:`Print Term` and :cmd:`About`.
 
-.. cmd:: Print All.
+.. cmd:: Print All
 
 This command displays information about the current state of the
 environment, including sections and modules.
@@ -63,13 +63,13 @@ environment, including sections and modules.
 Variants:
 
 
-.. cmdv:: Inspect @num.
+.. cmdv:: Inspect @num
    :name: Inspect
 
 This command displays the :n:`@num` last objects of the
 current environment, including sections and modules.
 
-.. cmdv:: Print Section @ident.
+.. cmdv:: Print Section @ident
 
 The name :n:`@ident` should correspond to a currently open section,
 this command displays the objects defined since the beginning of this
@@ -89,32 +89,32 @@ handling flags, options and tables are given below.
 
 .. TODO : flag is not a syntax entry
 
-.. cmd:: Set @flag.
+.. cmd:: Set @flag
 
 This command switches :n:`@flag` on. The original state of :n:`@flag` is restored
 when the current module ends.
 
 Variants:
 
-.. cmdv:: Local Set @flag.
+.. cmdv:: Local Set @flag
 
 This command switches :n:`@flag` on. The original state
 of :n:`@flag` is restored when the current *section* ends.
 
-.. cmdv:: Global Set @flag.
+.. cmdv:: Global Set @flag
 
 This command switches :n:`@flag` on. The original state
 of :n:`@flag` is *not* restored at the end of the module. Additionally, if
 set in a file, :n:`@flag` is switched on when the file is `Require`-d.
 
-.. cmdv:: Export Set @flag.
+.. cmdv:: Export Set @flag
 
    This command switches :n:`@flag` on. The original state
    of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
    is switched on when this module is imported.
 
 
-.. cmd:: Unset @flag.
+.. cmd:: Unset @flag
 
 This command switches :n:`@flag` off. The original state of :n:`@flag` is restored
 when the current module ends.
@@ -122,30 +122,30 @@ when the current module ends.
 
 Variants:
 
-.. cmdv:: Local Unset @flag.
+.. cmdv:: Local Unset @flag
 
 This command switches :n:`@flag` off. The original
 state of :n:`@flag` is restored when the current *section* ends.
 
-.. cmdv:: Global Unset @flag.
+.. cmdv:: Global Unset @flag
 
 This command switches :n:`@flag` off. The original
 state of :n:`@flag` is *not* restored at the end of the module. Additionally,
 if set in a file, :n:`@flag` is switched off when the file is `Require`-d.
 
-.. cmdv:: Export Unset @flag.
+.. cmdv:: Export Unset @flag
 
    This command switches :n:`@flag` off. The original state
    of :n:`@flag` is restored at the end of the current module, but :n:`@flag`
    is switched off when this module is imported.
 
 
-.. cmd:: Test @flag.
+.. cmd:: Test @flag
 
 This command prints whether :n:`@flag` is on or off.
 
 
-.. cmd:: Set @option @value.
+.. cmd:: Set @option @value
 
 This command sets :n:`@option` to :n:`@value`. The original value of ` option` is
 restored when the current module ends.
@@ -155,26 +155,26 @@ Variants:
 
 .. TODO : option and value are not syntax entries
 
-.. cmdv:: Local Set @option @value.
+.. cmdv:: Local Set @option @value
 
 This command sets :n:`@option` to :n:`@value`. The
 original value of :n:`@option` is restored at the end of the module.
 
-.. cmdv:: Global Set @option @value.
+.. cmdv:: Global Set @option @value
 
 This command sets :n:`@option` to :n:`@value`. The
 original value of :n:`@option` is *not* restored at the end of the module.
 Additionally, if set in a file, :n:`@option` is set to value when the file
 is `Require`-d.
 
-.. cmdv:: Export Set @option.
+.. cmdv:: Export Set @option
 
    This command set :n:`@option` to :n:`@value`. The original state
    of :n:`@option` is restored at the end of the current module, but :n:`@option`
    is set to :n:`@value` when this module is imported.
 
 
-.. cmd::  Unset @option.
+.. cmd::  Unset @option
 
    This command turns off :n:`@option`.
 
@@ -182,48 +182,48 @@ is `Require`-d.
 Variants:
 
 
-.. cmdv:: Local Unset @option.
+.. cmdv:: Local Unset @option
 
    This command turns off :n:`@option`. The original state of :n:`@option` is restored when the current
    *section* ends.
 
-.. cmdv:: Global Unset @option.
+.. cmdv:: Global Unset @option
 
    This command turns off :n:`@option`. The original state of :n:`@option` is *not* restored at the end of the
    module. Additionally, if unset in a file, :n:`@option` is reset to its
    default value when the file is `Require`-d.
 
-.. cmdv:: Export Unset @option.
+.. cmdv:: Export Unset @option
 
    This command turns off :n:`@option`. The original state of :n:`@option` is restored at the end of the
    current module, but :n:`@option` is set to its default value when this module
    is imported.
 
 
-.. cmd:: Test @option.
+.. cmd:: Test @option
 
 This command prints the current value of :n:`@option`.
 
 
 .. TODO : table is not a syntax entry
 
-.. cmd:: Add @table @value.
+.. cmd:: Add @table @value
    :name: Add `table` `value`
 
-.. cmd:: Remove @table @value.
+.. cmd:: Remove @table @value
    :name: Remove `table` `value`
 
-.. cmd:: Test @table @value.
+.. cmd:: Test @table @value
    :name: Test `table` `value`
 
-.. cmd:: Test @table for @value.
+.. cmd:: Test @table for @value
    :name: Test `table` for `value`
 
-.. cmd:: Print Table @table.
+.. cmd:: Print Table @table
 
 These are  general commands for tables.
 
-.. cmd:: Print Options.
+.. cmd:: Print Options
 
 This command lists all available flags, options and tables.
 
@@ -231,7 +231,7 @@ This command lists all available flags, options and tables.
 Variants:
 
 
-.. cmdv:: Print Tables.
+.. cmdv:: Print Tables
 
 This is a synonymous of ``Print Options``.
 
@@ -241,7 +241,7 @@ This is a synonymous of ``Print Options``.
 Requests to the environment
 -------------------------------
 
-.. cmd:: Check @term.
+.. cmd:: Check @term
 
 This command displays the type of :n:`@term`. When called in proof mode, the
 term is checked in the local context of the current subgoal.
@@ -251,14 +251,14 @@ Variants:
 
 .. TODO : selector is not a syntax entry
 
-.. cmdv:: @selector: Check @term.
+.. cmdv:: @selector: Check @term
 
 specifies on which subgoal to perform typing
 (see Section :ref:`invocation-of-tactics`).
 
 .. TODO : convtactic is not a syntax entry
 
-.. cmd:: Eval @convtactic in @term.
+.. cmd:: Eval @convtactic in @term
 
 This command performs the specified reduction on :n:`@term`, and displays
 the resulting term with its type. The term to be reduced may depend on
@@ -269,7 +269,7 @@ progress).
 See also: Section :ref:`performingcomputations`.
 
 
-.. cmd:: Compute @term.
+.. cmd:: Compute @term
 
 This command performs a call-by-value evaluation of term by using the
 bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in``
@@ -290,23 +290,23 @@ relies.
 Variants:
 
 
-.. cmdv:: Print Opaque Dependencies @qualid.
+.. cmdv:: Print Opaque Dependencies @qualid
 
 Displays the set of opaque constants :n:`@qualid` relies on in addition to
 the assumptions.
 
-.. cmdv:: Print Transparent Dependencies @qualid.
+.. cmdv:: Print Transparent Dependencies @qualid
 
 Displays the set of
 transparent constants :n:`@qualid` relies on in addition to the assumptions.
 
-.. cmdv:: Print All Dependencies @qualid.
+.. cmdv:: Print All Dependencies @qualid
 
 Displays all assumptions and constants :n:`@qualid` relies on.
 
 
 
-.. cmd:: Search @qualid.
+.. cmd:: Search @qualid
 
 This command displays the name and type of all objects (hypothesis of
 the current goal, theorems, axioms, etc) of the current context whose
@@ -323,7 +323,7 @@ There is no constant in the environment named qualid.
 
 Variants:
 
-.. cmdv:: Search @string.
+.. cmdv:: Search @string
 
 If :n:`@string` is a valid identifier, this command
 displays the name and type of all objects (theorems, axioms, etc) of
@@ -332,20 +332,20 @@ notation’s string denoting some reference :n:`@qualid` (referred to by its
 main symbol as in `"+"` or by its notation’s string as in `"_ + _"` or
 `"_ 'U' _"`, see Section :ref:`notations`), the command works like ``Search`` :n:`@qualid`.
 
-.. cmdv:: Search @string%@key.
+.. cmdv:: Search @string%@key
 
 The string string must be a notation or the main
 symbol of a notation which is then interpreted in the scope bound to
 the delimiting key :n:`@key` (see Section :ref:`LocalInterpretationRulesForNotations`).
 
-.. cmdv:: Search @term_pattern.
+.. cmdv:: Search @term_pattern
 
 This searches for all statements or types of
 definition that contains a subterm that matches the pattern
 `term_pattern` (holes of the pattern are either denoted by `_` or by
 `?ident` when non linear patterns are expected).
 
-.. cmdv:: Search { + [-]@term_pattern_string }.
+.. cmdv:: Search { + [-]@term_pattern_string }
 
 where
 :n:`@term_pattern_string` is a term_pattern, a string, or a string followed
@@ -357,15 +357,15 @@ correspond to valid identifiers. If a term_pattern or a string is
 prefixed by `-`, the search excludes the objects that mention that
 term_pattern or that string.
 
-.. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid } .
+.. cmdv:: Search @term_pattern_string … @term_pattern_string inside {+ @qualid }
 
 This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
 
-.. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid }.
+.. cmdv:: Search @term_pattern_string … @term_pattern_string outside {+ @qualid }
 
 This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
 
-.. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string.
+.. cmdv:: @selector: Search [-]@term_pattern_string … [-]@term_pattern_string
 
 This specifies the goal on which to search hypothesis (see
 Section :ref:`invocation-of-tactics`).
@@ -393,7 +393,7 @@ be combined with other variants presented here.
    may also be enclosed by optional ``[ ]`` delimiters.
 
 
-.. cmd:: SearchHead @term.
+.. cmd:: SearchHead @term
 
 This command displays the name and type of all hypothesis of the
 current goal (if any) and theorems of the current context whose
@@ -411,11 +411,11 @@ useful to remind the user of the name of library lemmas.
 
 Variants:
 
-.. cmdv:: SearchHead @term inside {+ @qualid }.
+.. cmdv:: SearchHead @term inside {+ @qualid }
 
 This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
 
-.. cmdv:: SearchHead term outside {+ @qualid }.
+.. cmdv:: SearchHead term outside {+ @qualid }
 
 This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
 
@@ -426,7 +426,7 @@ Error messages:
 No module :n:`@qualid` has been required
 (see Section :ref:`compiled-files`).
 
-.. cmdv:: @selector: SearchHead @term.
+.. cmdv:: @selector: SearchHead @term
 
 This specifies the goal on which to
 search hypothesis (see Section :ref:`invocation-of-tactics`).
@@ -437,7 +437,7 @@ here.
 .. note:: Up to |Coq| version 8.4, ``SearchHead`` was named ``Search``.
 
 
-.. cmd:: SearchPattern @term.
+.. cmd:: SearchPattern @term
 
 This command displays the name and type of all hypothesis of the
 current goal (if any) and theorems of the current context whose
@@ -472,15 +472,15 @@ must occur in two places by using pattern variables `?ident`.
 Variants:
 
 
-.. cmdv:: SearchPattern @term inside {+ @qualid } .
+.. cmdv:: SearchPattern @term inside {+ @qualid }
 
 This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
 
-.. cmdv:: SearchPattern @term outside {+ @qualid }.
+.. cmdv:: SearchPattern @term outside {+ @qualid }
 
 This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
 
-.. cmdv:: @selector: SearchPattern @term.
+.. cmdv:: @selector: SearchPattern @term
 
 This specifies the goal on which to
 search hypothesis (see Section :ref:`invocation-of-tactics`). By default the 1st goal is
@@ -489,7 +489,7 @@ here.
 
 
 
-.. cmdv:: SearchRewrite @term.
+.. cmdv:: SearchRewrite @term
 
 This command displays the name and type of all hypothesis of the
 current goal (if any) and theorems of the current context whose
@@ -507,15 +507,15 @@ expression term. Holes in term are denoted by “_”.
 Variants:
 
 
-.. cmdv:: SearchRewrite term inside {+ @qualid }.
+.. cmdv:: SearchRewrite term inside {+ @qualid }
 
 This restricts the search to constructions defined in the modules named by the given :n:`qualid` sequence.
 
-.. cmdv:: SearchRewrite @term outside {+ @qualid }.
+.. cmdv:: SearchRewrite @term outside {+ @qualid }
 
 This restricts the search to constructions not defined in the modules named by the given :n:`qualid` sequence.
 
-.. cmdv:: @selector: SearchRewrite @term.
+.. cmdv:: @selector: SearchRewrite @term
 
 This specifies the goal on which to
 search hypothesis (see Section :ref:`invocation-of-tactics`). By default the 1st goal is
@@ -534,7 +534,7 @@ here.
    this blacklist.
 
 
-.. cmd:: Locate @qualid.
+.. cmd:: Locate @qualid
 
 This command displays the full name of objects whose name is a prefix
 of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in
@@ -560,15 +560,15 @@ qualified name spaces of |Coq|: terms, modules, Ltac, etc.
 Variants:
 
 
-.. cmdv:: Locate Term @qualid.
+.. cmdv:: Locate Term @qualid
 
 As Locate but restricted to terms.
 
-.. cmdv:: Locate Module @qualid.
+.. cmdv:: Locate Module @qualid
 
 As Locate but restricted to modules.
 
-.. cmdv:: Locate Ltac @qualid.
+.. cmdv:: Locate Ltac @qualid
 
 As Locate but restricted to tactics.
 
@@ -589,7 +589,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard
 (and default) extension of |Coq|’s script files is .v.
 
 
-.. cmd:: Load @ident.
+.. cmd:: Load @ident
 
 This command loads the file named :n:`ident`.v, searching successively in
 each of the directories specified in the *loadpath*. (see Section
@@ -601,16 +601,16 @@ command cannot be used inside a proof either.
 Variants:
 
 
-.. cmdv:: Load @string.
+.. cmdv:: Load @string
 
 Loads the file denoted by the string :n:`@string`, where
 string is any complete filename. Then the `~` and .. abbreviations are
 allowed as well as shell variables. If no extension is specified, |Coq|
 will use the default extension ``.v``.
 
-.. cmdv:: Load Verbose @ident.
+.. cmdv:: Load Verbose @ident
 
-.. cmdv:: Load Verbose @string.
+.. cmdv:: Load Verbose @string
 
 Display, while loading,
 the answers of |Coq| to each command (including tactics) contained in
@@ -634,7 +634,7 @@ Chapter :ref:`thecoqcommands` for documentation on how to compile a file). A com
 file is a particular case of module called *library file*.
 
 
-.. cmd:: Require @qualid.
+.. cmd:: Require @qualid
 
 This command looks in the loadpath for a file containing module :n:`@qualid`
 and adds the corresponding module to the environment of |Coq|. As
@@ -656,7 +656,7 @@ several files match, one of them is picked in an unspecified fashion.
 
 Variants:
 
-.. cmdv:: Require Import @qualid.
+.. cmdv:: Require Import @qualid
 
 This loads and declares the module :n:`@qualid`
 and its dependencies then imports the contents of :n:`@qualid` as described
@@ -668,13 +668,13 @@ through a sequence of ``Require Export``.  If the module required has
 already been loaded, ``Require Import`` :n:`@qualid` simply imports it, as ``Import``
 :n:`@qualid` would.
 
-.. cmdv:: Require Export @qualid.
+.. cmdv:: Require Export @qualid
 
 This command acts as ``Require Import`` :n:`@qualid`,
 but if a further module, say `A`, contains a command ``Require Export`` `B`,
 then the command ``Require Import`` `A` also imports the module `B.`
 
-.. cmdv:: Require [Import | Export] {+ @qualid }.
+.. cmdv:: Require [Import | Export] {+ @qualid }
 
 This loads the
 modules named by the :n:`qualid` sequence and their recursive
@@ -683,7 +683,7 @@ dependencies. If
 all the recursive dependencies that were marked or transitively marked
 as ``Export``.
 
-.. cmdv:: From @dirpath Require @qualid.
+.. cmdv:: From @dirpath Require @qualid
 
 This command acts as ``Require``, but picks
 any library whose absolute name is of the form dirpath.dirpath’.qualid
@@ -737,14 +737,14 @@ that the commands ``Import`` and ``Export`` alone can be used inside modules
 See also: Chapter :ref:`thecoqcommands`
 
 
-.. cmd:: Print Libraries.
+.. cmd:: Print Libraries
 
 This command displays the list of library files loaded in the
 current |Coq| session. For each of these libraries, it also tells if it
 is imported.
 
 
-.. cmd:: Declare ML Module {+ @string } .
+.. cmd:: Declare ML Module {+ @string }
 
 This commands loads the OCaml compiled files
 with names given by the :n:`@string` sequence
@@ -758,7 +758,7 @@ version of OCaml that supports native Dynlink (≥ 3.11).
 Variants:
 
 
-.. cmdv:: Local Declare ML Module {+ @string }.
+.. cmdv:: Local Declare ML Module {+ @string }
 
 This variant is not
 exported to the modules that import the module where they occur, even
@@ -774,7 +774,7 @@ Error messages:
 
 
 
-.. cmd:: Print ML Modules.
+.. cmd:: Print ML Modules
 
 This prints the name of all OCaml modules loaded with ``Declare
 ML Module``. To know from where these module were loaded, the user
@@ -792,12 +792,12 @@ for practical purposes. Such commands are only meant to be issued in
 the toplevel, and using them in source files is discouraged.
 
 
-.. cmd:: Pwd.
+.. cmd:: Pwd
 
 This command displays the current working directory.
 
 
-.. cmd:: Cd @string.
+.. cmd:: Cd @string
 
 This command changes the current directory according to :n:`@string` which
 can be any valid path.
@@ -806,13 +806,13 @@ can be any valid path.
 Variants:
 
 
-.. cmdv:: Cd.
+.. cmdv:: Cd
 
 Is equivalent to Pwd.
 
 
 
-.. cmd:: Add LoadPath @string as @dirpath.
+.. cmd:: Add LoadPath @string as @dirpath
 
 This command is equivalent to the command line option
 ``-Q`` :n:`@string` :n:`@dirpath`. It adds the physical directory string to the current
@@ -821,14 +821,14 @@ This command is equivalent to the command line option
 Variants:
 
 
-.. cmdv:: Add LoadPath @string.
+.. cmdv:: Add LoadPath @string
 
 Performs as Add LoadPath :n:`@string` as :n:`@dirpath` but
 for the empty directory path.
 
 
 
-.. cmd:: Add Rec LoadPath @string as @dirpath.
+.. cmd:: Add Rec LoadPath @string as @dirpath
 
 This command is equivalent to the command line option
 ``-R`` :n:`@string` :n:`@dirpath`. It adds the physical directory string and all its
@@ -837,19 +837,19 @@ subdirectories to the current |Coq| loadpath.
 Variants:
 
 
-.. cmdv:: Add Rec LoadPath @string.
+.. cmdv:: Add Rec LoadPath @string
 
 Works as ``Add Rec LoadPath`` :n:`@string` as :n:`@dirpath` but for the empty
 logical directory path.
 
 
 
-.. cmd:: Remove LoadPath @string.
+.. cmd:: Remove LoadPath @string
 
 This command removes the path :n:`@string` from the current |Coq| loadpath.
 
 
-.. cmd:: Print LoadPath.
+.. cmd:: Print LoadPath
 
 This command displays the current |Coq| loadpath.
 
@@ -857,26 +857,26 @@ This command displays the current |Coq| loadpath.
 Variants:
 
 
-.. cmdv:: Print LoadPath @dirpath.
+.. cmdv:: Print LoadPath @dirpath
 
 Works as ``Print LoadPath`` but displays only
 the paths that extend the :n:`@dirpath` prefix.
 
 
-.. cmd:: Add ML Path @string.
+.. cmd:: Add ML Path @string
 
 This command adds the path :n:`@string` to the current OCaml
 loadpath (see the command `Declare ML Module`` in Section :ref:`compiled-files`).
 
 
-.. cmd:: Add Rec ML Path @string.
+.. cmd:: Add Rec ML Path @string
 
 This command adds the directory :n:`@string` and all its subdirectories to
 the current OCaml loadpath (see the command ``Declare ML Module``
 in Section :ref:`compiled-files`).
 
 
-.. cmd:: Print ML Path @string.
+.. cmd:: Print ML Path @string
 
 This command displays the current OCaml loadpath. This
 command makes sense only under the bytecode version of ``coqtop``, i.e.
@@ -885,13 +885,13 @@ using option ``-byte``
 
 .. _locate-file:
 
-.. cmd:: Locate File @string.
+.. cmd:: Locate File @string
 
 This command displays the location of file string in the current
 loadpath. Typically, string is a .cmo or .vo or .v file.
 
 
-.. cmd:: Locate Library @dirpath.
+.. cmd:: Locate Library @dirpath
 
 This command gives the status of the |Coq| module dirpath. It tells if
 the module is loaded and if not searches in the load path for a module
@@ -908,7 +908,7 @@ interactively, they cannot be part of a vernacular file loaded via
 ``Load`` or compiled by ``coqc``.
 
 
-.. cmd:: Reset @ident.
+.. cmd:: Reset @ident
 
 This command removes all the objects in the environment since :n:`@ident`
 was introduced, including :n:`@ident`. :n:`@ident` may be the name of a defined or
@@ -922,14 +922,14 @@ Error messages:
 
 Variants:
 
-.. cmd:: Reset Initial.
+.. cmd:: Reset Initial
 
 Goes back to the initial state, just after the start
 of the interactive session.
 
 
 
-.. cmd:: Back.
+.. cmd:: Back
 
 This commands undoes all the effects of the last vernacular command.
 Commands read from a vernacular file via a ``Load`` are considered as a
@@ -945,7 +945,7 @@ the statement of this proof.
 Variants:
 
 
-.. cmdv:: Back @num.
+.. cmdv:: Back @num
 
 Undoes :n:`@num` vernacular commands. As for Back, some extra
 commands may be undone in order to reach an adequate state. For
@@ -961,7 +961,7 @@ Error messages:
 
 The user wants to undo more commands than available in the history.
 
-.. cmd:: BackTo @num.
+.. cmd:: BackTo @num
 
 This command brings back the system to the state labeled :n:`@num`,
 forgetting the effect of all commands executed after this state. The
@@ -975,7 +975,7 @@ necessary.
 Variants:
 
 
-.. cmdv:: Backtrack @num @num @num.
+.. cmdv:: Backtrack @num @num @num
 
 `Backtrack` is a *deprecated* form of
 `BackTo` which allows explicitly manipulating the proof environment. The
@@ -1005,12 +1005,12 @@ Quitting and debugging
 --------------------------
 
 
-.. cmd:: Quit.
+.. cmd:: Quit
 
 This command permits to quit |Coq|.
 
 
-.. cmd:: Drop.
+.. cmd:: Drop
 
 This is used mostly as a debug facility by |Coq|’s implementors and does
 not concern the casual user. This command permits to leave |Coq|
@@ -1046,19 +1046,19 @@ to |Coq| with the command:
 
 .. TODO : command is not a syntax entry
 
-.. cmd:: Time @command.
+.. cmd:: Time @command
 
 This command executes the vernacular command :n:`@command` and displays the
 time needed to execute it.
 
 
-.. cmd:: Redirect @string @command.
+.. cmd:: Redirect @string @command
 
 This command executes the vernacular command :n:`@command`, redirecting its
 output to ":n:`@string`.out".
 
 
-.. cmd:: Timeout @num @command.
+.. cmd:: Timeout @num @command
 
 This command executes the vernacular command :n:`@command`. If the command
 has not terminated after the time specified by the :n:`@num` (time
@@ -1072,7 +1072,7 @@ displayed.
    were passed to a :cmd:`Timeout` command. Commands already starting by a
    :cmd:`Timeout` are unaffected.
 
-.. cmd:: Fail @command.
+.. cmd:: Fail @command
 
 For debugging scripts, sometimes it is desirable to know
 whether a command or a tactic fails. If the given :n:`@command`
@@ -1162,7 +1162,7 @@ as numbers, and for reflection-based tactics. The commands to fine-
 tune the reduction strategies and the lazy conversion algorithm are
 described first.
 
-.. cmd:: Opaque {+ @qualid }.
+.. cmd:: Opaque {+ @qualid }
 
 This command has an effect on unfoldable constants, i.e. on constants
 defined by ``Definition`` or ``Let`` (with an explicit body), or by a command
@@ -1191,7 +1191,7 @@ Error messages:
 There is no constant referred by :n:`@qualid` in the environment.
 Nevertheless, if you asked ``Opaque`` `foo` `bar` and if `bar` does not exist, `foo` is set opaque.
 
-.. cmd:: Transparent {+ @qualid }.
+.. cmd:: Transparent {+ @qualid }
 
 This command is the converse of `Opaque`` and it applies on unfoldable
 constants to restore their unfoldability after an Opaque command.
@@ -1222,7 +1222,7 @@ See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`, :
 
 .. _vernac-strategy:
 
-.. cmd:: Strategy @level [ {+ @qualid } ].
+.. cmd:: Strategy @level [ {+ @qualid } ]
 
 This command generalizes the behavior of Opaque and Transparent
 commands. It is used to fine-tune the strategy for unfolding
@@ -1254,7 +1254,7 @@ regarding sections and modules is the same as for the ``Transparent`` and
 ``Opaque`` commands.
 
 
-.. cmd:: Print Strategy @qualid.
+.. cmd:: Print Strategy @qualid
 
 This command prints the strategy currently associated to :n:`@qualid`. It
 fails if :n:`@qualid` is not an unfoldable reference, that is, neither a
@@ -1271,13 +1271,13 @@ Error messages:
 Variants:
 
 
-.. cmdv:: Print Strategies.
+.. cmdv:: Print Strategies
 
 Print all the currently non-transparent strategies.
 
 
 
-.. cmd:: Declare Reduction @ident := @convtactic.
+.. cmd:: Declare Reduction @ident := @convtactic
 
 This command allows giving a short name to a reduction expression, for
 instance lazy beta delta [foo bar]. This short name can then be used
@@ -1301,8 +1301,8 @@ Controlling the locality of commands
 -----------------------------------------
 
 
-.. cmd:: Local @command.
-.. cmd:: Global @command.
+.. cmd:: Local @command
+.. cmd:: Global @command
 
 Some commands support a Local or Global prefix modifier to control the
 scope of their effect. There are four kinds of commands: