Fix error messages and make them consistent.

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

5 files changed, 29 insertions, 28 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`.