Clean-up around cmd documentation.

In particular, remove trailing dots.

5 files changed, 158 insertions, 156 deletions

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: