Command Arguments: standardizing format of error messages and American spelling.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14810 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 17 insertions, 18 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 47a2e462dd..472d7903b8 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1148,7 +1148,7 @@ In case one wants that some arguments of a given object (constant,
 inductive types, constructors, assumptions, local or not) are always
 inferred by Coq, one may declare once and for all which are the expected
 implicit arguments of this object. There are two ways to do this,
-a-priori and a-posteriori. 
+a priori and a posteriori.
 
 \subsubsection{Implicit Argument Binders}
 
@@ -1190,7 +1190,7 @@ usual implicit arguments disambiguation syntax.
 
 \subsubsection{Declaring Implicit Arguments}
 
-To set implicit arguments for a constant a-posteriori, one can use the
+To set implicit arguments for a constant a posteriori, one can use the
 command:
 \begin{quote}
 \tt Arguments {\qualid} \nelist{\possiblybracketedident}{}
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 925ff693a7..5de4ffd169 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,5 +1,5 @@
 The command has indeed failed with message:
-=> Error: to rename arguments the "rename" flag must be specified
+=> Error: To rename arguments the "rename" flag must be specified.
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
@@ -95,12 +95,12 @@ Expands to: Constant Top.myplus
 myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
-=> Error: All arguments lists must declare the same names
+=> Error: All arguments lists must declare the same names.
 The command has indeed failed with message:
-=> Error: The following arguments are not declared: x
+=> Error: The following arguments are not declared: x.
 The command has indeed failed with message:
-=> Error: Arguments names must be distinct
+=> Error: Arguments names must be distinct.
 The command has indeed failed with message:
-=> Error: Argument z cannot be declared implicit
+=> Error: Argument z cannot be declared implicit.
 The command has indeed failed with message:
-=> Error: Extra argument y
+=> Error: Extra argument y.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a04b167cbb..b38c3bddc1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -775,18 +775,18 @@ let vernac_declare_arguments local r l nargs flags =
   let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
   let names, rest = List.hd names, List.tl names in
   if List.exists ((<>) names) rest then
-    error "All arguments lists must declare the same names";
+    error "All arguments lists must declare the same names.";
   if not (Util.list_distinct (List.filter ((<>) Anonymous) names)) then
-    error "Arguments names must be distinct";
+    error "Arguments names must be distinct.";
   let sr = smart_global r in
   let inf_names =
     Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in
   let string_of_name = function Anonymous -> "_" | Name id -> string_of_id id in
   let rec check li ld = match li, ld with
     | [], [] -> ()
-    | [], x::_ -> error ("Extra argument " ^ string_of_name x)
+    | [], x::_ -> error ("Extra argument " ^ string_of_name x ^ ".")
     | l, [] -> error ("The following arguments are not declared: " ^
-       (String.concat ", " (List.map string_of_name l)))
+       (String.concat ", " (List.map string_of_name l)) ^ ".")
     | _::li, _::ld -> check li ld in
   if l <> [[]] then
     List.iter (fun l -> check inf_names l) (names :: rest);
@@ -806,7 +806,7 @@ let vernac_declare_arguments local r l nargs flags =
       let sr', impl = Util.list_fold_map (fun b -> function
         | (Anonymous, _,_, true, max), Name id -> assert false
         | (Name x, _,_, true, _), Anonymous ->
-            error ("Argument "^string_of_id x^" cannot be declared implicit")
+            error ("Argument "^string_of_id x^" cannot be declared implicit.")
         | (Name iid, _,_, true, max), Name id ->
            b || iid <> id, Some (ExplByName id, max, false)
         | _ -> b, None)
@@ -815,7 +815,7 @@ let vernac_declare_arguments local r l nargs flags =
       some_renaming_specified l in
   if some_renaming_specified then
     if not (List.mem `Rename flags) then
-      error "to rename arguments the \"rename\" flag must be specified"
+      error "To rename arguments the \"rename\" flag must be specified."
     else Arguments_renaming.rename_arguments local sr names_decl;
   (* All other infos are in the first item of l *)
   let l = List.hd l in
@@ -836,7 +836,7 @@ let vernac_declare_arguments local r l nargs flags =
   else if some_implicits_specified || List.mem `ClearImplicits flags then
     vernac_declare_implicits local r implicits;
   if nargs >= 0 && nargs < List.fold_left max 0 rargs then
-    error "The \"/\" option must be places after the last \"!\"";
+    error "The \"/\" option must be placed after the last \"!\".";
   let rec narrow = function
     | #Tacred.simpl_flag as x :: tl -> x :: narrow tl
     | [] -> [] | _ :: tl -> narrow tl in
@@ -845,8 +845,7 @@ let vernac_declare_arguments local r l nargs flags =
     match sr with
     | ConstRef _ as c ->
        Tacred.set_simpl_behaviour local c (rargs, nargs, flags)
-    | _ -> error "Simpl behaviour can be declared for constants only"
-;;
+    | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
 
 let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
@@ -1372,7 +1371,7 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) =
   Proof.transaction p 
     (fun () -> Proof_global.Bullet.put p bullet);
   (* Makes the focus visible in emacs by re-printing the goal. *)
-  if !Flags.print_emacs then print_subgoals ();;
+  if !Flags.print_emacs then print_subgoals ()
 
 
 let vernac_show = function