Fix error messages and make them consistent.

All the error messages start with a capitalized letter and end with a dot.

11 files changed, 164 insertions, 155 deletions

diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index 75d797201..7dc36b557 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -591,24 +591,24 @@ generated expression and the original.
 Here is a summary of the error messages corresponding to each
 situation:
 
-.. exn:: The constructor @ident expects @num arguments
+.. exn:: The constructor @ident expects @num arguments.
 
    The variable ident is bound several times in pattern termFound a constructor
    of inductive type term while a constructor of term is expectedPatterns are
    incorrect (because constructors are not applied to the correct number of the
    arguments, because they are not linear or they are wrongly typed).
 
-.. exn:: Non exhaustive pattern-matching
+.. exn:: Non exhaustive pattern-matching.
 
    The pattern matching is not exhaustive.
 
 .. exn:: The elimination predicate term should be of arity @num (for non \
-         dependent case) or @num (for dependent case)
+         dependent case) or @num (for dependent case).
 
    The elimination predicate provided to match has not the expected arity.
 
 .. exn:: Unable to infer a match predicate
-         Either there is a type incompatibility or the problem involves dependencies
+         Either there is a type incompatibility or the problem involves dependencies.
 
    There is a type mismatch between the different branches. The user should
    provide an elimination predicate.
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 9a08657f9..3f4ef2232 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -129,16 +129,16 @@ Declaration of Coercions
   Declares the construction denoted by `qualid` as a coercion between
   the two given classes.
 
-  .. exn:: @qualid not declared
-  .. exn:: @qualid is already a coercion
-  .. exn:: Funclass cannot be a source class
-  .. exn:: @qualid is not a function
-  .. exn:: Cannot find the source class of @qualid
-  .. exn:: Cannot recognize @class as a source class of @qualid
-  .. exn:: @qualid does not respect the uniform inheritance condition
+  .. exn:: @qualid not declared.
+  .. exn:: @qualid is already a coercion.
+  .. exn:: Funclass cannot be a source class.
+  .. exn:: @qualid is not a function.
+  .. exn:: Cannot find the source class of @qualid.
+  .. exn:: Cannot recognize @class as a source class of @qualid.
+  .. exn:: @qualid does not respect the uniform inheritance condition.
   .. exn:: Found target class ... instead of ...
 
-  .. warn:: Ambiguous path
+  .. warn:: Ambiguous path.
 
     When the coercion `qualid` is added to the inheritance graph, non
     valid coercion paths are ignored; they are signaled by a warning
@@ -211,7 +211,7 @@ declaration, this constructor is declared as a coercion.
   function with type :g:`forall (x₁:T₁)..(xₙ:Tₙ)(y:C x₁..xₙ),D t₁..tₘ`,
   and we declare it as an identity coercion between ``C`` and ``D``.
 
-  .. exn:: @class must be a transparent constant
+  .. exn:: @class must be a transparent constant.
 
   .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident.
 
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 20e40c550..e03431320 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -56,7 +56,7 @@ Messages from ``omega``
 When ``omega`` does not solve the goal, one of the following errors
 is generated:
 
-.. exn:: omega can't solve this system
+.. exn:: omega can't solve this system.
 
   This may happen if your goal is not quantifier-free (if it is
   universally quantified, try ``intros`` first; if it contains
@@ -65,20 +65,20 @@ is generated:
   operators unknown from ``omega``. Finally, your goal may be really
   wrong!
 
-.. exn:: omega: Not a quantifier-free goal
+.. exn:: omega: Not a quantifier-free goal.
 
   If your goal is universally quantified, you should first apply
   ``intro`` as many time as needed.
 
-.. exn:: omega: Unrecognized predicate or connective: @ident
+.. exn:: omega: Unrecognized predicate or connective: @ident.
 
 .. exn:: omega: Unrecognized atomic proposition: ...
 
-.. exn:: omega: Can't solve a goal with proposition variables
+.. exn:: omega: Can't solve a goal with proposition variables.
 
-.. exn:: omega: Unrecognized proposition
+.. exn:: omega: Unrecognized proposition.
 
-.. exn:: omega: Can't solve a goal with non-linear products
+.. exn:: omega: Can't solve a goal with non-linear products.
 
 .. exn:: omega: Can't solve a goal with equality on type ...
 
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index be30d1bc4..3ac7361c7 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -151,7 +151,8 @@ Program Definition
    obligations. Once solved using the commands shown below, it binds the
    final |Coq| term to the name ``ident`` in the environment.
 
-   .. exn:: @ident already exists (Program Definition)
+   .. exn:: @ident already exists.
+      :name: @ident already exists. (Program Definition)
 
    .. cmdv:: Program Definition @ident : @type := @term
 
@@ -349,7 +350,7 @@ Frequently Asked Questions
 ---------------------------
 
 
-.. exn:: Ill-formed recursive definition
+.. exn:: Ill-formed recursive definition.
 
   This error can happen when one tries to define a function by structural
   recursion on a subset object, which means the |Coq| function looks like:
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index ae666a0d4..11308e7e7 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -171,21 +171,21 @@ performs the simplification in the hypothesis named :n:`@ident`.
 Error messages:
 
 
-.. exn:: not a valid ring equation
+.. exn:: Not a valid ring equation.
 
   The conclusion of the goal is not provable in the corresponding ring theory.
 
-.. exn:: arguments of ring_simplify do not have all the same type 
+.. exn:: Arguments of ring_simplify do not have all the same type.
   
   ``ring_simplify`` cannot simplify terms of several rings at the same
   time. Invoke the tactic once per ring structure.
 
-.. exn:: cannot find a declared ring structure over @term
+.. exn:: Cannot find a declared ring structure over @term.
 
   No ring has been declared for the type of the terms to be simplified.
   Use ``Add Ring`` first.
 
-.. exn:: cannot find a declared ring structure for equality @term 
+.. exn:: Cannot find a declared ring structure for equality @term.
 
   Same as above is the case of the ``ring`` tactic.
 
@@ -396,18 +396,18 @@ div :n:`@term`
 
 Error messages:
 
-.. exn:: bad ring structure
+.. exn:: Bad ring structure.
 
   The proof of the ring structure provided is not
   of the expected type.
 
-.. exn:: bad lemma for decidability of equality
+.. exn:: Bad lemma for decidability of equality.
 
   The equality function
   provided in the case of a computational ring has not the expected
   type.
 
-.. exn:: ring operation should be declared as a morphism
+.. exn:: Ring operation should be declared as a morphism.
 
   A setoid associated to the carrier of the ring structure has been found, 
   but the ring operation should be declared as morphism. See :ref:`tactics-enabled-on-user-provided-relations`.
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index d6bbcd37e..8cafe84a0 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -689,11 +689,11 @@ presence of partial application of `wrong` in the body of
 For now, dependent cases are not treated for non structurally
 terminating functions.
 
-.. exn:: The recursive argument must be specified
-.. exn:: No argument name @ident
-.. exn:: Cannot use mutual definition with well-founded recursion or measure
+.. exn:: The recursive argument must be specified.
+.. exn:: No argument name @ident.
+.. exn:: Cannot use mutual definition with well-founded recursion or measure.
 
-.. warn:: Cannot define graph for @ident
+.. warn:: Cannot define graph for @ident.
 
     The generation of the graph relation (`R_ident`) used to compute the induction scheme of ident
     raised a typing error. Only `ident` is defined; the induction scheme
@@ -703,12 +703,12 @@ terminating functions.
       which ``Function`` cannot deal with yet.
     - the definition is not a *pattern-matching tree* as explained above.
 
-.. warn:: Cannot define principle(s) for @ident
+.. warn:: Cannot define principle(s) for @ident.
 
      The generation of the graph relation (`R_ident`) succeeded but the induction principle
      could not be built. Only `ident` is defined. Please report.
 
-.. warn:: Cannot build functional inversion principle
+.. warn:: Cannot build functional inversion principle.
 
      `functional inversion` will not be available for the function.
 
@@ -820,7 +820,7 @@ Section :ref:`gallina-definitions`).
     Notice the difference between the value of `x’` and `x’’` inside section
     `s1` and outside.
 
-    .. exn:: This is not the last opened section
+    .. exn:: This is not the last opened section.
 
 **Remarks:**
 
@@ -906,11 +906,11 @@ Reserved commands inside an interactive module
    functor) its components (constants, inductive types, submodules etc.)
    are now available through the dot notation.
 
-    .. exn:: No such label @ident
+    .. exn:: No such label @ident.
 
-    .. exn:: Signature components for label @ident do not match
+    .. exn:: Signature components for label @ident do not match.
 
-    .. exn:: This is not the last opened module
+    .. exn:: This is not the last opened module.
 
 .. cmd:: Module @ident := @module_expression.
 
@@ -965,7 +965,7 @@ Reserved commands inside an interactive module type:
 
    This command closes the interactive module type `ident`.
 
-   .. exn:: This is not the last opened module type
+   .. exn:: This is not the last opened module type.
 
 .. cmd:: Module Type @ident := @module_type.
 
@@ -1225,7 +1225,7 @@ qualified name.
        When the module containing the command Export qualid
        is imported, qualid is imported as well.
 
-    .. exn:: @qualid is not a module
+    .. exn:: @qualid is not a module.
 
     .. warn:: Trying to mask the absolute name @qualid!
 
@@ -1525,6 +1525,7 @@ force the given argument to be guessed by replacing it by “_”. If
 possible, the correct argument will be automatically generated.
 
 .. exn:: Cannot infer a term for this placeholder.
+   :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments)
 
    |Coq| was not able to deduce an instantiation of a “_”.
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index c87bdd190..44bf255bb 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -557,7 +557,8 @@ has type :token:`type`.
    the global context. The fact asserted by *term* is thus assumed as a
    postulate.
 
-.. exn:: @ident already exists (Axiom)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Axiom)
 
 .. cmdv:: Parameter @ident : @term.
    :name: Parameter
@@ -596,7 +597,8 @@ will be unknown and every object using this variable will be explicitly
 parametrized (the variable is *discharged*). Using the ``Variable`` command out
 of any section is equivalent to using ``Local Parameter``.
 
-.. exn:: @ident already exists (Variable)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Variable)
 
 .. cmdv:: Variable {+ @ident } : @term.
 
@@ -646,7 +648,8 @@ Section :ref:`typing-rules`.
    This command binds :token:`term` to the name :token:`ident` in the environment,
    provided that :token:`term` is well-typed.
 
-.. exn:: @ident already exists (Definition)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Definition)
 
 .. cmdv:: Definition @ident : @term := @term.
 
@@ -676,7 +679,7 @@ Section :ref:`typing-rules`.
 
 These are synonyms of the Definition forms.
 
-.. exn:: The term @term has type @type while it is expected to have type @type
+.. exn:: The term @term has type @type while it is expected to have type @type.
 
 See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
 
@@ -690,7 +693,8 @@ prefixed by the let-in definition ``let`` :token:`ident` ``:=`` :token:`term`
 ``in``. Using the ``Let`` command out of any section is equivalent to using
 ``Local Definition``.
 
-.. exn:: @ident already exists (Let)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Let)
 
 .. cmdv:: Let @ident : @term := @term.
 
@@ -803,9 +807,9 @@ and to prove that if any natural number :g:`n` satisfies :g:`P` its double
 successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the
 structural induction principle we got for :g:`nat`.
 
-.. exn:: Non strictly positive occurrence of @ident in @type
+.. exn:: Non strictly positive occurrence of @ident in @type.
 
-.. exn:: The conclusion of @type is not valid; it must be built from @ident
+.. exn:: The conclusion of @type is not valid; it must be built from @ident.
 
 Parametrized inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -864,7 +868,7 @@ that it disallows recursive definition of types (in particular lists cannot
 be defined with the Variant keyword). No induction scheme is generated for
 this variant, unless :opt:`Nonrecursive Elimination Schemes` is set.
 
-.. exn:: The @num th argument of @ident must be @ident in @type
+.. exn:: The @num th argument of @ident must be @ident in @type.
 
 New from Coq V8.1
 +++++++++++++++++
@@ -1246,9 +1250,10 @@ After the statement is asserted, Coq needs a proof. Once a proof of
 validated, the proof is generalized into a proof of forall , :token:`type` and
 the theorem is bound to the name :token:`ident` in the environment.
 
-.. exn:: The term @term has type @type which should be Set, Prop or Type
+.. exn:: The term @term has type @type which should be Set, Prop or Type.
 
-.. exn:: @ident already exists (Theorem)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Theorem)
 
    The name you provided is already defined. You have then to choose
    another name.
@@ -1334,7 +1339,8 @@ the theorem is bound to the name :token:`ident` in the environment.
    When the proof is completed it should be validated and put in the environment
    using the keyword Qed.
 
-.. exn:: @ident already exists (Qed)
+.. exn:: @ident already exists.
+   :name: @ident already exists. (Qed)
 
 .. note::
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 2d08acc40..f74106abc 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -288,8 +288,8 @@ focused goals with:
       nothing (i.e. it cannot make some progress). ``par:`` can only be used at
       the toplevel of a tactic expression.
 
-   .. exn:: No such goal
-      :name: No such goal (goal selector)
+   .. exn:: No such goal.
+      :name: No such goal. (Goal selector)
 
    .. TODO change error message index entry
 
@@ -348,7 +348,7 @@ We can check if a tactic made progress with:
    to one of the focused subgoal produced subgoals equal to the initial
    goals (up to syntactical equality), then an error of level 0 is raised.
 
-   .. exn:: Failed to progress
+   .. exn:: Failed to progress.
 
 Backtracking branching
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -389,7 +389,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics:
    :n:`first [:@expr__1 | ... | @expr__n]` behaves, in each goal, as the the first
    :n:`v__i` to have *at least* one success.
 
-   .. exn:: Error message: No applicable tactic
+   .. exn:: No applicable tactic.
 
    .. tacv:: first @expr
 
@@ -478,7 +478,7 @@ one* success:
       whether a second success exists, and may run further effects
       immediately.
 
-   .. exn:: This tactic has more than one success
+   .. exn:: This tactic has more than one success.
 
 Checking the failure
 ~~~~~~~~~~~~~~~~~~~~
@@ -516,7 +516,7 @@ among a panel of tactics:
    each goal independently, if it doesn’t solve the goal then it tries to
    apply :n:`v__2` and so on. It fails if there is no solving tactic.
 
-   .. exn:: Cannot solve the goal
+   .. exn:: Cannot solve the goal.
 
    .. tacv:: solve @expr
 
@@ -760,11 +760,11 @@ We can carry out pattern matching on terms with:
    branches or inside the right-hand side of the selected branch even if it
    has backtracking points.
 
-   .. exn:: No matching clauses for match
+   .. exn:: No matching clauses for match.
 
       No pattern can be used and, in particular, there is no :n:`_` pattern.
 
-   .. exn:: Argument of match does not evaluate to a term
+   .. exn:: Argument of match does not evaluate to a term.
 
       This happens when :n:`@expr` does not denote a term.
 
@@ -844,7 +844,7 @@ We can make pattern matching on goals using the following expression:
    branches or combinations of hypotheses, or inside the right-hand side of
    the selected branch even if it has backtracking points.
 
-   .. exn:: No matching clauses for match goal
+   .. exn:: No matching clauses for match goal.
 
       No clause succeeds, i.e. all matching patterns, if any, fail at the
       application of the right-hand-side.
@@ -891,7 +891,7 @@ produce subgoals but generates a term to be used in tactic expressions:
    match expression. This expression evaluates replaces the hole of the
    value of :n:`@ident` by the value of :n:`@expr`.
 
-   .. exn:: not a context variable
+   .. exn:: Not a context variable.
 
 Generating fresh hypothesis names
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1001,7 +1001,7 @@ Testing boolean expressions
          all:let n:= numgoals in guard n<4.
          Fail all:let n:= numgoals in guard n=2.
 
-   .. exn:: Condition not satisfied
+   .. exn:: Condition not satisfied.
 
 Proving a subgoal as a separate lemma
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1051,8 +1051,8 @@ Proving a subgoal as a separate lemma
          with tactics is fragile, and explicitly named and reused subterms
          don’t play well with asynchronous proofs.
 
-   .. exn:: Proof is not complete
-      :name: Proof is not complete (abstract)
+   .. exn:: Proof is not complete.
+      :name: Proof is not complete. (abstract)
 
 Tactic toplevel definitions
 ---------------------------
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 53205b619..8643742ae 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -34,7 +34,7 @@ terms of λ-calculus, known as the *Curry-Howard isomorphism*
 terms are called *proof terms*.
 
 
-.. exn:: No focused proof
+.. exn:: No focused proof.
 
 Coq raises this error message when one attempts to use a proof editing command
 out of the proof editing mode.
@@ -68,7 +68,7 @@ proof term to the declared name of the original goal. This name is
 added to the environment as an opaque constant.
 
 
-.. exn:: Attempt to save an incomplete proof
+.. exn:: Attempt to save an incomplete proof.
 
 .. note::
 
@@ -239,7 +239,7 @@ the previous proof development, or to the |Coq| toplevel if no other
 proof was edited.
 
 
-.. exn:: No focused proof (No proof-editing in progress)
+.. exn:: No focused proof (No proof-editing in progress).
 
 
 
@@ -298,7 +298,7 @@ Repeats Undo :n:`@num` times.
 This command restores the proof editing process to the original goal.
 
 
-.. exn:: No focused proof to restart
+.. exn:: No focused proof to restart.
 
 
 .. cmd:: Focus.
@@ -349,14 +349,14 @@ This focuses on the :n:`@num` th subgoal to prove.
 
 Error messages:
 
-.. exn:: This proof is focused, but cannot be unfocused this way
+.. exn:: This proof is focused, but cannot be unfocused this way.
 
 You are trying to use ``}`` but the current subproof has not been fully solved.
 
-.. exn:: No such goal
-   :name: No such goal (focusing)
+.. exn:: No such goal.
+   :name: No such goal. (Focusing)
 
-.. exn:: Brackets only support the single numbered goal selector
+.. exn:: Brackets only support the single numbered goal selector.
 
 See also error messages about bullets below.
 
@@ -409,11 +409,11 @@ The following example script illustrates all these features:
     assumption.
 
 
-.. exn:: Wrong bullet @bullet1 : Current bullet @bullet2 is not finished.
+.. exn:: Wrong bullet @bullet1: Current bullet @bullet2 is not finished.
 
 Before using bullet :n:`@bullet1` again, you should first finish proving the current focused goal. Note that :n:`@bullet1` and :n:`@bullet2` may be the same.
 
-.. exn:: Wrong bullet @bullet1 : Bullet @bullet2 is mandatory here.
+.. exn:: Wrong bullet @bullet1: Bullet @bullet2 is mandatory here.
 
 You must put :n:`@bullet2` to focus next goal. No other bullet is allowed here.
 
@@ -449,8 +449,8 @@ This command displays the current goals.
 
 Displays only the :n:`@num`-th subgoal.
 
-.. exn:: No such goal
-.. exn:: No focused proof
+.. exn:: No such goal.
+.. exn:: No focused proof.
 
 .. cmdv:: Show @ident.
 
@@ -524,7 +524,7 @@ This variant displays a template of the Gallina
 
      Show Match nat.
 
-.. exn:: Unknown inductive type
+.. exn:: Unknown inductive type.
 
 .. _ShowUniverses:
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 238e56197..73961167b 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -92,7 +92,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
   the ``n``-th non dependent premise of the ``term``, as determined by the type
   of ``term``.
 
-  .. exn:: No such binder
+  .. exn:: No such binder.
 
 + A bindings list can also be a simple list of terms :n:`{* term}`.
   In that case the references to which these terms correspond are
@@ -226,19 +226,20 @@ useful to advanced users.
 
      Defined.
 
-.. exn:: invalid argument
+.. exn:: Invalid argument.
 
    The tactic ``refine`` does not know what to do with the term you gave.
 
-.. exn:: Refine passed ill-formed term
+.. exn:: Refine passed ill-formed term.
 
    The term you gave is not a valid proof (not easy to debug in general). This
    message may also occur in higher-level tactics that call ``refine``
    internally.
 
-.. exn:: Cannot infer a term for this placeholder
+.. exn:: Cannot infer a term for this placeholder.
+   :name: Cannot infer a term for this placeholder. (refine)
 
-   There is a hole in the term you gave which type cannot be inferred. Put a
+   There is a hole in the term you gave whose type cannot be inferred. Put a
    cast around it.
 
 .. tacv:: simple refine @term
@@ -528,8 +529,8 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
    constructor of :g:`I`, then ``constructor i`` is equivalent to
    ``intros; apply c``:sub:`i`.
 
-.. exn:: Not an inductive product
-.. exn:: Not enough constructors
+.. exn:: Not an inductive product.
+.. exn:: Not enough constructors.
 
 .. tacv:: constructor
 
@@ -562,7 +563,7 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
    to :n:`intros; constructor 1 with @bindings_list.` It is typically used in
    the case of an existential quantification :math:`\exists`:g:`x, P(x).`
 
-.. exn:: Not an inductive goal with 1 constructor
+.. exn:: Not an inductive goal with 1 constructor.
 
 .. tacv:: exists @bindings_list
 
@@ -579,7 +580,7 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below.
    Then, they are respectively equivalent to ``constructor 1`` and
    ``constructor 2``.
 
-.. exn:: Not an inductive goal with 2 constructors
+.. exn:: Not an inductive goal with 2 constructors.
 
 .. tacv:: left with @bindings_list
 .. tacv:: right with @bindings_list
@@ -656,7 +657,7 @@ be applied or the goal is not head-reducible.
    This applies ``intro`` but forces :n:`@ident` to be the name of the
    introduced hypothesis.
 
-.. exn:: name @ident is already used
+.. exn:: Name @ident is already used.
 
 .. note:: If a name used by intro hides the base name of a global
    constant then the latter can still be referred to by a qualified name
@@ -675,7 +676,7 @@ be applied or the goal is not head-reducible.
    `(@ident:term)` and discharges the variable named `ident` of the current
    goal.
 
-.. exn:: No such hypothesis in current goal
+.. exn:: No such hypothesis in current goal.
 
 .. tacv:: intros until @num
 
@@ -704,7 +705,7 @@ be applied or the goal is not head-reducible.
    too so as to respect the order of dependencies between hypotheses.
    Note that :n:`intro at bottom` is a synonym for :n:`intro` with no argument.
 
-.. exn:: No such hypothesis : @ident.
+.. exn:: No such hypothesis: @ident.
 
 .. tacv:: intro @ident after @ident
 .. tacv:: intro @ident before @ident
@@ -883,7 +884,7 @@ quantification or an implication.
    This tactic expects :n:`@ident` to be a local definition then clears its
    body. Otherwise said, this tactic turns a definition into an assumption.
 
-.. exn:: @ident is not a local definition
+.. exn:: @ident is not a local definition.
 
 .. tacv:: clear - {+ @ident}
 
@@ -950,9 +951,9 @@ the inverse of :tacn:`intro`.
    This moves ident at the bottom of the local context (at the end of the
    context).
 
-.. exn:: No such hypothesis
-.. exn:: Cannot move @ident after @ident : it occurs in the type of @ident
-.. exn:: Cannot move @ident after @ident : it depends on @ident
+.. exn:: No such hypothesis.
+.. exn:: Cannot move @ident after @ident : it occurs in the type of @ident.
+.. exn:: Cannot move @ident after @ident : it depends on @ident.
 
 .. example::
    .. coqtop:: all
@@ -979,8 +980,8 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
    particular, the target identifiers may contain identifiers that exist in the
    source context, as long as the latter are also renamed by the same tactic.
 
-.. exn:: No such hypothesis
-.. exn:: @ident is already used
+.. exn:: No such hypothesis.
+.. exn:: @ident is already used.
 
 .. tacn:: set (@ident := @term)
    :name: set
@@ -992,7 +993,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged.
    first checks that all subterms matching the pattern are compatible before
    doing the replacement using the leftmost subterm matching the pattern.
 
-.. exn:: The variable @ident is already defined
+.. exn:: The variable @ident is already defined.
 
 .. tacv:: set (@ident := @term ) in @goal_occurrences
 
@@ -1110,7 +1111,7 @@ Controlling the proof flow
    :g:`U` [2]_. The subgoal :g:`U` comes first in the list of subgoals remaining to
    prove.
 
-.. exn:: Not a proposition or a type
+.. exn:: Not a proposition or a type.
 
    Arises when the argument form is neither of type :g:`Prop`, :g:`Set` nor
    :g:`Type`.
@@ -1125,8 +1126,8 @@ Controlling the proof flow
    This tactic behaves like :n:`assert` but applies tactic to solve the subgoals
    generated by assert.
 
-   .. exn:: Proof is not complete
-      :name: Proof is not complete (assert)
+   .. exn:: Proof is not complete.
+      :name: Proof is not complete. (assert)
 
 .. tacv:: assert form as intro_pattern
 
@@ -1147,7 +1148,7 @@ Controlling the proof flow
    the type of :g:`term`. This is deprecated in favor of :n:`pose proof`. If the
    head of term is :n:`@ident`, the tactic behaves as :n:`specialize @term`.
 
-   .. exn:: Variable @ident is already declared
+   .. exn:: Variable @ident is already declared.
 
 .. tacv:: eassert form as intro_pattern by tactic
    :name: eassert
@@ -1239,8 +1240,8 @@ Controlling the proof flow
    the goal. The :n:`as` clause is especially useful in this case to immediately
    introduce the instantiated statement as a local hypothesis.
 
-   .. exn:: @ident is used in hypothesis @ident
-   .. exn:: @ident is used in conclusion
+   .. exn:: @ident is used in hypothesis @ident.
+   .. exn:: @ident is used in conclusion.
 
 .. tacn:: generalize @term
    :name: generalize
@@ -1364,7 +1365,7 @@ goals cannot be closed with :g:`Qed` but only with :g:`Admitted`.
    a singleton inductive type (e.g. :g:`True` or :g:`x=x`), or two contradictory
    hypotheses.
 
-.. exn:: No such assumption
+.. exn:: No such assumption.
 
 .. tacv:: contradiction @ident
 
@@ -1570,9 +1571,9 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       intros n H.
       induction n.
 
-.. exn:: Not an inductive product
+.. exn:: Not an inductive product.
 
-.. exn:: Unable to find an instance for the variables @ident ... @ident
+.. exn:: Unable to find an instance for the variables @ident ... @ident.
 
    Use in this case the variant :tacn:`elim ... with` below.
 
@@ -1846,8 +1847,8 @@ See also: :ref:`advanced-recursive-functions`
   :ref:`functional-scheme`
   :tacn:`inversion`
 
-.. exn:: Cannot find induction information on @qualid
-.. exn:: Not the right number of induction arguments
+.. exn:: Cannot find induction information on @qualid.
+.. exn:: Not the right number of induction arguments.
 
 .. tacv:: functional induction (@qualid {+ @term}) as @disj_conj_intro_pattern using @term with @bindings_list
 
@@ -1880,8 +1881,8 @@ See also: :ref:`advanced-recursive-functions`
    :n:`@ident` is first introduced in the local context using
    :n:`intros until @ident`.
 
-.. exn:: No primitive equality found
-.. exn:: Not a discriminable equality
+.. exn:: No primitive equality found.
+.. exn:: Not a discriminable equality.
 
 .. tacv:: discriminate @num
 
@@ -1909,7 +1910,7 @@ See also: :ref:`advanced-recursive-functions`
    the form :n:`@term <> @term`, this behaves as
    :n:`intro @ident; discriminate @ident`.
 
-   .. exn:: No discriminable equalities
+   .. exn:: No discriminable equalities.
 
 .. tacn:: injection @term
    :name: injection
@@ -1958,10 +1959,10 @@ the use of a sigma type is avoided.
    then :n:`injection @ident` first introduces the hypothesis in the local
    context using :n:`intros until @ident`.
 
-.. exn:: Not a projectable equality but a discriminable one
-.. exn:: Nothing to do, it is an equality between convertible @terms
-.. exn:: Not a primitive equality
-.. exn:: Nothing to inject
+.. exn:: Not a projectable equality but a discriminable one.
+.. exn:: Nothing to do, it is an equality between convertible @terms.
+.. exn:: Not a primitive equality.
+.. exn:: Nothing to inject.
 
 .. tacv:: injection @num
 
@@ -1987,7 +1988,7 @@ the use of a sigma type is avoided.
    If the current goal is of the form :n:`@term <> @term` , this behaves as
    :n:`intro @ident; injection @ident`.
 
-   .. exn:: goal does not satisfy the expected preconditions
+   .. exn:: goal does not satisfy the expected preconditions.
 
 .. tacv:: injection @term {? with @bindings_list} as {+ @intro_pattern}
 .. tacv:: injection @num as {+ intro_pattern}
@@ -2406,7 +2407,7 @@ Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification,
 and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new
 subgoals.
 
-.. exn:: The @term provided does not end with an equation
+.. exn:: The @term provided does not end with an equation.
 
 .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal.
 
@@ -2484,7 +2485,7 @@ subgoals.
    the assumption, or if its symmetric form occurs. It is equivalent to
    :n:`cut @term = @term; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`.
 
-.. exn:: @terms do not have convertible types
+.. exn:: @terms do not have convertible types.
 
 .. tacv:: replace @term with @term by tactic
 
@@ -2629,7 +2630,7 @@ as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
    with `U` providing that `U` is well-formed and that `T` and `U` are
    convertible.
 
-.. exn:: Not convertible
+.. exn:: Not convertible.
 
 
 .. tacv:: change @term with @term
@@ -2642,7 +2643,7 @@ as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see
   This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term by @term`
   in the current goal. The terms :n:`@term` and :n:`@term` must be convertible.
 
-.. exn:: Too few occurrences
+.. exn:: Too few occurrences.
 
 .. tacv:: change @term in @ident
 .. tacv:: change @term with @term in @ident
@@ -2817,7 +2818,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    definition (say :g:`t`) and then reduces
    :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules.
 
-.. exn:: Not reducible
+.. exn:: Not reducible.
 
 .. tacn:: hnf
    :name: hnf
@@ -2944,7 +2945,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms
    matching :n:`@pattern` in the current goal.
 
-   .. exn:: Too few occurrences
+   .. exn:: Too few occurrences.
 
 .. tacv:: simpl @qualid
 .. tacv:: simpl @string
@@ -2974,7 +2975,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :n:`@qualid` refers in the current goal and then replaces it with its
    :math:`\beta`:math:`\iota`-normal form.
 
-.. exn:: @qualid does not denote an evaluable constant
+.. exn:: @qualid does not denote an evaluable constant.
 
 .. tacv:: unfold @qualid in @ident
 
@@ -2991,9 +2992,9 @@ the conversion in hypotheses :n:`{+ @ident}`.
    The lists :n:`{+, @num}` specify the occurrences of :n:`@qualid` to be
    unfolded. Occurrences are located from left to right.
 
-   .. exn:: bad occurrence number of @qualid
+   .. exn:: Bad occurrence number of @qualid.
 
-   .. exn:: @qualid does not occur
+   .. exn:: @qualid does not occur.
 
 .. tacv:: unfold @string
 
@@ -3083,7 +3084,7 @@ Conversion tactics applied to hypotheses
 
    Example: :n:`unfold not in (Type of H1) (Type of H3)`.
 
-.. exn:: No such hypothesis : ident.
+.. exn:: No such hypothesis: @ident.
 
 
 .. _automation:
@@ -3908,7 +3909,7 @@ match against it.
    Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps
    in case you have partially applied constructors in your goal.
 
-.. exn:: I don’t know how to handle dependent equality
+.. exn:: I don’t know how to handle dependent equality.
 
   The decision procedure managed to find a proof of the goal or of a
   discriminable equality but this proof could not be built in Coq because of
@@ -3939,7 +3940,7 @@ succeeds, and results in an error otherwise.
    This tactic checks whether its arguments are equal modulo alpha
    conversion and casts.
 
-.. exn:: Not equal
+.. exn:: Not equal.
 
 .. tacn:: unify @term @term
    :name: unify
@@ -3947,7 +3948,7 @@ succeeds, and results in an error otherwise.
    This tactic checks whether its arguments are unifiable, potentially
    instantiating existential variables.
 
-.. exn:: Not unifiable
+.. exn:: Not unifiable.
 
 .. tacv:: unify @term @term with @ident
 
@@ -3961,7 +3962,7 @@ succeeds, and results in an error otherwise.
    variable. Existential variables are uninstantiated variables generated
    by :tacn:`eapply` and some other tactics.
 
-.. exn:: Not an evar
+.. exn:: Not an evar.
 
 .. tacn:: has_evar @term
    :name: has_evar
@@ -3970,7 +3971,7 @@ succeeds, and results in an error otherwise.
    a subterm. Unlike context patterns combined with ``is_evar``, this tactic
    scans all subterms, including those under binders.
 
-.. exn:: No evars
+.. exn:: No evars.
 
 .. tacn:: is_var @term
    :name: is_var
@@ -3978,7 +3979,7 @@ succeeds, and results in an error otherwise.
    This tactic checks whether its argument is a variable or hypothesis in
    the current goal context or in the opened sections.
 
-.. exn:: Not a variable or hypothesis
+.. exn:: Not a variable or hypothesis.
 
 
 .. _equality:
@@ -4005,7 +4006,7 @@ This tactic applies to a goal that has the form :g:`t=u`. It checks that `t`
 and `u` are convertible and then solves the goal. It is equivalent to apply
 :tacn:`refl_equal`.
 
-.. exn:: The conclusion is not a substitutive equation
+.. exn:: The conclusion is not a substitutive equation.
 
 .. exn:: Unable to unify ... with ...
 
@@ -4123,8 +4124,8 @@ Inversion
 available after a ``Require Import FunInd``.
 
 
-.. exn:: Hypothesis @ident must contain at least one Function
-.. exn:: Cannot find inversion information for hypothesis @ident
+.. exn:: Hypothesis @ident must contain at least one Function.
+.. exn:: Cannot find inversion information for hypothesis @ident.
 
   This error may be raised when some inversion lemma failed to be generated by
   Function.
@@ -4155,7 +4156,7 @@ function :n:`@ident`. This function must be a fixpoint on a simple recursive
 datatype: see :ref:`quote` for the full details.
 
 
-.. exn:: quote: not a simple fixpoint
+.. exn:: quote: not a simple fixpoint.
 
   Happens when quote is not able to perform inversion properly.
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 672c7a0fe..0d160a025 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -23,9 +23,9 @@ defined object referred by :n:`@qualid`.
 Error messages:
 
 
-.. exn:: @qualid not a defined object
+.. exn:: @qualid not a defined object.
 
-.. exn:: Universe instance should have length :n:`num`.
+.. exn:: Universe instance should have length @num.
 
 .. exn:: This object does not support universe names.
 
@@ -336,7 +336,7 @@ of the name of library lemmas.
 Error messages:
 
 
-.. exn:: The reference @qualid was not found in the current environment
+.. exn:: The reference @qualid was not found in the current environment.
 
 There is no constant in the environment named qualid.
 
@@ -440,7 +440,7 @@ This restricts the search to constructions not defined in the modules named by t
 
 Error messages:
 
-.. exn:: Module/section @qualid not found
+.. exn:: Module/section @qualid not found.
 
 No module :n:`@qualid` has been required
 (see Section :ref:`compiled-files`).
@@ -637,11 +637,11 @@ the loaded file See also: Section :ref:`controlling-display`.
 
 Error messages:
 
-.. exn:: Can’t find file @ident on loadpath
+.. exn:: Can’t find file @ident on loadpath.
 
-.. exn:: Load is not supported inside proofs
+.. exn:: Load is not supported inside proofs.
 
-.. exn:: Files processed by Load cannot leave open proofs
+.. exn:: Files processed by Load cannot leave open proofs.
 
 .. _compiled-files:
 
@@ -713,15 +713,15 @@ comes from a given package by making explicit its absolute root.
 
 Error messages:
 
-.. exn:: Cannot load qualid: no physical path bound to dirpath
+.. exn:: Cannot load qualid: no physical path bound to dirpath.
 
-.. exn:: Cannot find library foo in loadpath
+.. exn:: Cannot find library foo in loadpath.
 
 The command did not find the
 file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a
 directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`).
 
-.. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid
+.. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid.
 
 The command tried to load library file :n:`@ident`.vo that
 depends on some specific version of library :n:`@qualid` which is not the
@@ -729,13 +729,13 @@ one already loaded in the current |Coq| session. Probably `ident.v` was
 not properly recompiled with the last version of the file containing
 module :n:`@qualid`.
 
-.. exn:: Bad magic number
+.. exn:: Bad magic number.
 
 The file `ident.vo` was found but either it is not a
 |Coq| compiled module, or it was compiled with an incompatible
 version of |Coq|.
 
-.. exn:: The file `ident.vo` contains library dirpath and not library dirpath’
+.. exn:: The file `ident.vo` contains library dirpath and not library dirpath’.
 
 The library file `dirpath’` is indirectly required by the
 ``Require`` command but it is bound in the current loadpath to the
@@ -743,7 +743,7 @@ file `ident.vo` which was bound to a different library name `dirpath` at
 the time it was compiled.
 
 
-.. exn:: Require is not allowed inside a module or a module type
+.. exn:: Require is not allowed inside a module or a module type.
 
 This command
 is not allowed inside a module or a module type being defined. It is
@@ -787,9 +787,9 @@ if outside a section.
 
 Error messages:
 
-.. exn:: File not found on loadpath : @string
+.. exn:: File not found on loadpath: @string.
 
-.. exn:: Loading of ML object file forbidden in a native Coq
+.. exn:: Loading of ML object file forbidden in a native Coq.
 
 
 
@@ -937,7 +937,7 @@ over the name of a module or of an object inside a module.
 
 Error messages:
 
-.. exn:: @ident: no such entry
+.. exn:: @ident: no such entry.
 
 Variants:
 
@@ -976,7 +976,7 @@ before that proof.
 Error messages:
 
 
-.. exn:: Invalid backtrack
+.. exn:: Invalid backtrack.
 
 The user wants to undo more commands than available in the history.
 
@@ -1012,7 +1012,7 @@ three numbers represent the following:
 Error messages:
 
 
-.. exn:: Invalid backtrack
+.. exn:: Invalid backtrack.
 
 
 The destination state label is unknown.
@@ -1205,7 +1205,7 @@ See also: sections :ref:`performingcomputations`, :ref:`tactics-automatizing`, :
 Error messages:
 
 
-.. exn:: The reference @qualid was not found in the current environment
+.. exn:: The reference @qualid was not found in the current environment.
 
 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.
@@ -1231,7 +1231,7 @@ used.
 Error messages:
 
 
-.. exn:: The reference @qualid was not found in the current environment
+.. exn:: The reference @qualid was not found in the current environment.
 
 There is no constant referred by :n:`@qualid` in the environment.