From 1ed5cc920523fc8e7ea61bb3962b235a310dfa71 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 24 Apr 2018 11:59:50 +0200
Subject: Fix error messages and make them consistent.

All the error messages start with a capitalized letter and end with a dot.
---
 doc/sphinx/addendum/program.rst | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/addendum/program.rst')

diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index be30d1bc4a..3ac7361c77 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:
-- 
cgit v1.2.3


From 5e22cf0783c9272158df92b90faedc37f6e47066 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 24 Apr 2018 11:59:51 +0200
Subject: Clean-up around cmd documentation.

In particular, remove trailing dots.
---
 doc/sphinx/addendum/program.rst | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'doc/sphinx/addendum/program.rst')

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
-- 
cgit v1.2.3