Uniformisation du format des messages d'erreur (commencent par une

majuscule - si pas un ident ou un terme - et se terminent par un point).
Restent quelques utilisations de "error" qui sont liées à des usages internes,
ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ?



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

17 files changed, 66 insertions, 56 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index f51cc0869..bd688bcdd 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -234,7 +234,7 @@ let rec interp_entry_name up_level s =
       try get_entry (get_univ "prim") s
       with _ ->
       try get_entry (get_univ "constr") s
-      with _ -> error ("Unknown entry "^s)
+      with _ -> error ("Unknown entry "^s^".")
     in
     let o = object_of_typed_entry e in
     let t = type_of_typed_entry e in
@@ -254,7 +254,7 @@ let get_tactic_entry n =
   else if 1<=n && n<5 then
     weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n))
   else 
-    error ("Invalid Tactic Notation level: "^(string_of_int n))
+    error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
 
 (* Declaration of the tactic grammar rule *)
 
@@ -267,7 +267,7 @@ let add_tactic_entry (key,lev,prods,tac) =
   let rules = 
     if lev = 0 then begin
       if not (head_is_ident prods) then
-	error "Notation for simple tactic must start with an identifier";
+	error "Notation for simple tactic must start with an identifier.";
       let mkact s tac loc l =
 	(TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in
       make_rule univ (mkact key tac) mkprod prods
diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml
index 8c570b0fd..f9ca94ff6 100644
--- a/parsing/g_ascii_syntax.ml
+++ b/parsing/g_ascii_syntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 open Pp
 open Util
@@ -53,7 +53,7 @@ let interp_ascii_string dloc s =
       then int_of_string s
       else
 	user_err_loc (dloc,"interp_ascii_string",
-	  str "Expects a single character or a three-digits ascii code") in
+	  str "Expects a single character or a three-digits ascii code.") in
   interp_ascii dloc p
 
 let uninterp_ascii r =
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 476c0913f..b8dcf8e99 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -47,7 +47,7 @@ let rec index_and_rec_order_of_annot loc bl ann =
     | lids, (Some (loc, n), ro) ->
         if List.exists (fun (_, x) -> x = Name n) lids then
 	  Some (loc, n), ro
-        else user_err_loc(loc,"index_of_annot", Pp.str"no such fix variable")
+        else user_err_loc(loc,"index_of_annot", Pp.str"No such fix variable.")
     | _, (None, r) -> None, r
 
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
@@ -61,7 +61,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = Option.map (fun (aloc,_) ->
     Util.user_err_loc
       (aloc,"Constr:mk_cofixb",
-       Pp.str"Annotation forbidden in cofix expression")) (fst ann) in
+       Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
   let ty = match tyc with
       Some ty -> ty
     | None -> CHole (loc, None) in
@@ -326,7 +326,7 @@ GEXTEND Gram
           | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
           | _ -> Util.user_err_loc 
               (cases_pattern_expr_loc p, "compound_pattern",
-               Pp.str "Constructor expected"))
+               Pp.str "Constructor expected."))
       | p = pattern; "as"; id = ident ->
 	  CPatAlias (loc, p, id) ]
     | "1" LEFTA
diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml
index f12ab6bee..7cef2fac0 100644
--- a/parsing/g_intsyntax.ml
+++ b/parsing/g_intsyntax.ml
@@ -122,7 +122,7 @@ let int31_of_pos_bigint dloc n =
   RApp (dloc, ref_construct, List.rev (args 31 n))
 
 let error_negative dloc =
-  Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers")
+  Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
 
 let interp_int31 dloc n = 
   if is_pos_or_zero n then
@@ -212,7 +212,7 @@ let bigN_of_pos_bigint dloc n =
   result hght (word_of_pos_bigint dloc hght n)
   
 let bigN_error_negative dloc =
-  Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers")
+  Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
 
 let interp_bigN dloc n = 
   if is_pos_or_zero n then
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index deedf957d..c24534e2d 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -31,7 +31,7 @@ let my_int_of_string loc s =
     if n > 1024 * 2048 then raise Exit;
     n
   with Failure _ | Exit ->
-    Util.user_err_loc (loc,"",Pp.str "cannot support a so large number.")
+    Util.user_err_loc (loc,"",Pp.str "Cannot support a so large number.")
 
 GEXTEND Gram
   GLOBAL: 
@@ -89,7 +89,7 @@ GEXTEND Gram
   ;
   ne_string:
     [ [ s = STRING -> 
-        if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s
+        if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string."); s
     ] ]
   ;
   dirpath:
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index bea3929df..a1fd1649e 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -131,15 +131,15 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
       | _, Some x ->
           let ids = List.map snd (List.flatten (List.map pi1 bl)) in
           (try list_index (snd x) ids
-          with Not_found -> error "no such fix variable")
-      | _ -> error "cannot guess decreasing argument of fix" in
+          with Not_found -> error "No such fix variable.")
+      | _ -> error "Cannot guess decreasing argument of fix." in
   (id,n,CProdN(loc,bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
   let _ = Option.map (fun (aloc,_) ->
     Util.user_err_loc
       (aloc,"Constr:mk_cofix_tac",
-       Pp.str"Annotation forbidden in cofix expression")) ann in
+       Pp.str"Annotation forbidden in cofix expression.")) ann in
   (id,CProdN(loc,bl,ty))
 
 (* Functions overloaded by quotifier *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 83b238953..5f656ed5c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -113,7 +113,7 @@ let test_plurial_form = function
 
 let no_coercion loc (c,x) =
   if c then Util.user_err_loc
-    (loc,"no_coercion",Pp.str"no coercion allowed here");
+    (loc,"no_coercion",str"No coercion allowed here.");
   x
 
 (* Gallina declarations *)
@@ -271,7 +271,7 @@ GEXTEND Gram
 		    Some (loc, id)
 		    else Util.user_err_loc
                       (loc,"Fixpoint",
-                      Pp.str "No argument named " ++ Nameops.pr_id id))
+                       str "No argument named " ++ Nameops.pr_id id ++ str"."))
               | None -> 
 		  (* If there is only one argument, it is the recursive one, 
 		     otherwise, we search the recursive index later *)
@@ -311,7 +311,7 @@ GEXTEND Gram
           LocalRawAssum(l,ty) -> (l,ty)
         | LocalRawDef _ ->
             Util.user_err_loc
-              (loc,"fix_param",Pp.str"defined binder not allowed here")) ] ]
+              (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ]
   ;
 *)
   (* ... with coercions *)
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index a9f3fd487..e1e334be6 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -31,7 +31,7 @@ type xml = XmlTag of loc * string * attribute list * xml list
 let check_tags loc otag ctag =
   if otag <> ctag then
     user_err_loc (loc,"",str "closing xml tag " ++ str ctag ++ 
-      str "does not match open xml tag " ++ str otag)
+      str "does not match open xml tag " ++ str otag ++ str ".")
 
 let xml_eoi = (Gram.Entry.create "xml_eoi" : xml Gram.Entry.e)
 
@@ -55,11 +55,19 @@ GEXTEND Gram
   ;
 END
 
+(* Errors *)
+
+let error_expect_one_argument loc =
+  user_err_loc (loc,"",str "wrong number of arguments (expect one).")
+
+let error_expect_no_argument loc =
+  user_err_loc (loc,"",str "wrong number of arguments (expect none).")
+
 (* Interpreting attributes *)
 
 let nmtoken (loc,a) =
   try int_of_string a
-  with Failure _ -> user_err_loc (loc,"",str "nmtoken expected")
+  with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.")
   
 let interp_xml_attr_qualid = function
   | "uri", s -> qualid_of_string s
@@ -94,7 +102,7 @@ let sort_of_cdata (loc,a) = match a with
   | "Prop" -> RProp Null
   | "Set" -> RProp Pos
   | "Type" -> RType None
-  | _ -> user_err_loc (loc,"",str "sort expected")
+  | _ -> user_err_loc (loc,"",str "sort expected.")
 
 let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
 
@@ -188,18 +196,18 @@ let rec interp_xml_constr = function
       RCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2))
   | XmlTag (loc,"SORT",al,[]) ->
       RSort (loc, get_xml_sort al)
-  | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s)
+  | XmlTag (loc,s,_,_) ->
+      user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
 
 and interp_xml_tag s = function
   | XmlTag (loc,tag,al,xl) when tag=s -> (loc,al,xl)
   | XmlTag (loc,tag,_,_) -> user_err_loc (loc, "", 
-    str "Expect tag " ++ str s ++ str " but find " ++ str s)
+    str "Expect tag " ++ str s ++ str " but find " ++ str s ++ str ".")
 
 and interp_xml_constr_alias s x =
   match interp_xml_tag s x with
     | (_,_,[x]) -> interp_xml_constr x
-    | (loc,_,_) -> 
-        user_err_loc (loc,"",str "wrong number of arguments (expect one)")
+    | (loc,_,_) -> error_expect_one_argument loc
 
 and interp_xml_term x = interp_xml_constr_alias "term" x
 and interp_xml_type x = interp_xml_constr_alias "type" x
@@ -215,8 +223,7 @@ and interp_xml_substitution x = interp_xml_constr_alias "substitution" x
 and interp_xml_decl_alias s x =
   match interp_xml_tag s x with
     | (_,al,[x]) -> (get_xml_binder al, interp_xml_constr x)
-    | (loc,_,_) -> 
-        user_err_loc (loc,"",str "wrong number of arguments (expect one)")
+    | (loc,_,_) -> error_expect_one_argument loc
 
 and interp_xml_def x = interp_xml_decl_alias "def" x
 and interp_xml_decl x = interp_xml_decl_alias "decl" x
@@ -227,17 +234,17 @@ and interp_xml_recursionOrder x =
     match s with
 	"Structural" -> 
 	  (match l with [] -> RStructRec
-	     | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected none)"))
+	     | _ -> error_expect_no_argument loc)
       | "WellFounded" -> 
 	  (match l with
 	       [c] -> RWfRec (interp_xml_type c)
-	     | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
+	     | _ -> error_expect_one_argument loc)
       | "Measure" -> 
 	  (match l with
 	       [c] -> RMeasureRec (interp_xml_type c)
-	     | _ -> user_err_loc (loc, "", str "wrong number of arguments (expected one)"))
+	     | _ -> error_expect_one_argument loc)
       | _ ->
-          user_err_loc (locs,"",str "invalid recursion order")
+          user_err_loc (locs,"",str "Invalid recursion order.")
 
 and interp_xml_FixFunction x =
   match interp_xml_tag "FixFunction" x with
@@ -248,15 +255,15 @@ and interp_xml_FixFunction x =
   | (loc,al,[x1;x2]) ->
       ((Some (nmtoken (get_xml_attr "recIndex" al)), RStructRec),
        (get_xml_name al, interp_xml_type x1, interp_xml_body x2))
-  | (loc,_,_) -> 
-        user_err_loc (loc,"",str "wrong number of arguments (expect one)")
+  | (loc,_,_) ->
+      error_expect_one_argument loc
 
 and interp_xml_CoFixFunction x =
   match interp_xml_tag "CoFixFunction" x with
   | (loc,al,[x1;x2]) ->
       (get_xml_name al, interp_xml_type x1, interp_xml_body x2)
     | (loc,_,_) -> 
-        user_err_loc (loc,"",str "wrong number of arguments (expect one)")
+	error_expect_one_argument loc
 
 (* Interpreting tactic argument *)
 
@@ -266,7 +273,8 @@ let rec interp_xml_tactic_arg = function
   | XmlTag (loc,"CALL",al,xl) ->
       let ltacref = ltacref_of_cdata (get_xml_attr "uri" al) in
       TacCall(loc,ArgArg ltacref,List.map interp_xml_tactic_arg xl)
-  | XmlTag (loc,s,_,_) -> user_err_loc (loc,"", str "Unexpected tag " ++ str s)
+  | XmlTag (loc,s,_,_) ->
+      user_err_loc (loc,"", str "Unexpected tag " ++ str s ++ str ".")
 
 let parse_tactic_arg ch =
   interp_xml_tactic_arg
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index 5d57c49db..bfbe54c28 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -57,7 +57,7 @@ let pos_of_bignat dloc x =
 
 let error_non_positive dloc = 
   user_err_loc (dloc, "interp_positive",
-    str "Only strictly positive numbers in type \"positive\"")
+    str "Only strictly positive numbers in type \"positive\".")
 
 let interp_positive dloc n =
   if is_strictly_pos n then pos_of_bignat dloc n
@@ -113,7 +113,7 @@ let n_of_binnat dloc pos_or_neg n =
     RRef (dloc, glob_N0)
 
 let error_negative dloc =
-  user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\"")
+  user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".")
 
 let n_of_int dloc n =
   if is_pos_or_zero n then n_of_binnat dloc true n
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index f9c2f90dd..cee08f234 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -247,7 +247,7 @@ let get_entry (u, utab) s =
     Hashtbl.find utab s 
   with Not_found -> 
     errorlabstrm "Pcoq.get_entry"
-      (str "unknown grammar entry " ++ str u ++ str ":" ++ str s)
+      (str "Unknown grammar entry " ++ str u ++ str ":" ++ str s ++ str ".")
 
 let new_entry etyp (u, utab) s =
   let ename = u ^ ":" ^ s in
@@ -307,12 +307,12 @@ let get_generic_entry s =
   try
     object_of_typed_entry (Hashtbl.find utab s)
   with Not_found -> 
-    error ("unknown grammar entry "^u^":"^s)
+    error ("Unknown grammar entry "^u^":"^s^".")
 
 let get_generic_entry_type (u,utab) s =
   try type_of_typed_entry (Hashtbl.find utab s)
   with Not_found -> 
-    error ("unknown grammar entry "^u^":"^s)
+    error ("Unknown grammar entry "^u^":"^s^".")
 
 let force_entry_type (u, utab) s etyp =
   try
@@ -578,7 +578,7 @@ let error_level_assoc p current expected =
   errorlabstrm ""
     (str "Level " ++ int p ++ str " is already declared " ++
      pr_assoc current ++ str " associative while it is now expected to be " ++
-     pr_assoc expected ++ str " associative")
+     pr_assoc expected ++ str " associative.")
 
 let find_position_gen forpat ensure assoc lev =
   let ccurrent,pcurrent as current = List.hd !level_stack in
@@ -695,7 +695,7 @@ let compute_entry allow_create adjust forpat = function
   | ETPattern -> weaken_entry Constr.pattern, None, false
   | ETOther ("constr","annot") -> 
       weaken_entry Constr.annot, None, false
-  | ETConstrList _ -> error "List of entries cannot be registered"
+  | ETConstrList _ -> error "List of entries cannot be registered."
   | ETOther (u,n) ->
       let u = get_univ u in
       let e =
@@ -762,6 +762,6 @@ let coerce_reference_to_id = function
   | Ident (_,id) -> id
   | Qualid (loc,_) ->
       user_err_loc (loc, "coerce_reference_to_id",
-        str "This expression should be a simple identifier")
+        str "This expression should be a simple identifier.")
 
 let coerce_global_to_id = coerce_reference_to_id
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 912406f3f..ca8b97588 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -719,7 +719,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
       hov 1 (str "pattern" ++
         pr_arg (prlist_with_sep pr_coma (pr_with_occurrences pr_constr)) l)
         
-  | Red true -> error "Shouldn't be accessible from user"
+  | Red true -> error "Shouldn't be accessible from user."
   | ExtraRedExpr s -> str s
   | CbvVm -> str "vm_compute"
 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3d1eec4fe..2a0e755ff 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -58,7 +58,7 @@ let declare_extra_genarg_pprule (rawwit, f) (globwit, g) (wit, h) =
   let s = match unquote wit with
     | ExtraArgType s -> s 
     | _ -> error
-	"Can declare a pretty-printing rule only for extra argument types"
+	"Can declare a pretty-printing rule only for extra argument types."
   in
   let f prc prlc prtac x = f prc prlc prtac (out_gen rawwit x) in
   let g prc prlc prtac x = g prc prlc prtac (out_gen globwit x) in
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index bdbd74b0f..0a9447b46 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -219,7 +219,7 @@ let pr_located_qualid = function
   | ModuleType (qid,_) ->
       str "Module Type" ++ spc () ++ pr_sp (Nametab.full_name_modtype qid)
   | Undefined qid ->    
-      pr_qualid qid ++ str " is not a defined object"
+      pr_qualid qid ++ spc () ++ str "not a defined object."
 
 let print_located_qualid ref =
   let (loc,qid) = qualid_of_reference ref in
@@ -599,12 +599,12 @@ let read_sec_context r =
   let dir =
     try Nametab.locate_section qid
     with Not_found ->
-      user_err_loc (loc,"read_sec_context", str "Unknown section") in
+      user_err_loc (loc,"read_sec_context", str "Unknown section.") in
   let rec get_cxt in_cxt = function
     | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
         if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
     | (_,Lib.ClosedSection _)::rest ->
-        error "Cannot print the contents of a closed section"
+        error "Cannot print the contents of a closed section."
 	(* LEM: Actually, we could if we wanted to. *)
     | [] -> []
     | hd::rest -> get_cxt (hd::in_cxt) rest 
@@ -648,7 +648,7 @@ let print_name ref =
     print_leaf_entry true (oname,lobj)
   with Not_found ->
     errorlabstrm
-      "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object")
+      "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
 let print_opaque_name qid = 
   let env = Global.env () in
@@ -658,7 +658,7 @@ let print_opaque_name qid =
         if cb.const_body <> None then
 	  print_constant_with_infos cst
         else 
-	  error "not a defined constant"
+	  error "Not a defined constant."
     | IndRef (sp,_) ->
         print_inductive sp
     | ConstructRef cstr -> 
@@ -736,7 +736,8 @@ let index_of_class cl =
   try 
     fst (class_info cl)
   with _ -> 
-    errorlabstrm "index_of_class" (pr_class cl ++ str" is not a defined class")
+    errorlabstrm "index_of_class"
+      (pr_class cl ++ spc() ++ str "not a defined class.")
 
 let print_path_between cls clt = 
   let i = index_of_class cls in
@@ -746,7 +747,8 @@ let print_path_between cls clt =
       lookup_path_between (i,j) 
     with _ -> 
       errorlabstrm "index_cl_of_id"
-        (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt)
+        (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
+	 ++ str ".")
   in
   print_path ((i,j),p)
 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 6119f5d1e..f59f9f2f3 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -318,7 +318,7 @@ let rec pr_evars_int i = function
 
 let default_pr_subgoal n =
   let rec prrec p = function
-    | [] -> error "No such goal"
+    | [] -> error "No such goal."
     | g::rest ->
        	if p = 1 then
           let pg = default_pr_goal g in
diff --git a/parsing/search.ml b/parsing/search.ml
index 88b51907b..9670c2b87 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -150,7 +150,7 @@ let rec id_from_pattern = function
   | PVar id -> Nametab.locate (make_qualid [] (string_of_id id))
  *)
   | PApp (p,_) -> id_from_pattern p
-  | _ -> error "the pattern is not simple enough"
+  | _ -> error "The pattern is not simple enough."
 	
 let raw_pattern_search extra_filter display_function pat =
   let name = id_from_pattern pat in
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 6e8425d98..65b3a075e 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -206,7 +206,7 @@ EXTEND
         let t, g = Q_util.interp_entry_name loc e sep in
         TacNonTerm (loc, t, g, Some s)
       | s = STRING ->
-	if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal");
+	if s = "" then Util.user_err_loc (loc,"",Pp.str "Empty terminal.");
         TacTerm s
     ] ]
   ;
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 0b3dd75ad..29e30bca7 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -110,7 +110,7 @@ EXTEND
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]"; "->"; "["; e = Pcaml.expr; "]"
         -> 
-      if s = "" then Util.user_err_loc (loc,"",Pp.str "Command name is empty");
+      if s = "" then Util.user_err_loc (loc,"",Pp.str"Command name is empty.");
       (s,l,<:expr< fun () -> $e$ >>)
     ] ]
   ;