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

5 files changed, 51 insertions, 46 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c922503aa..304ac5d78 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -98,7 +98,7 @@ let ids_of_ctxt ctxt =
        (function c -> match kind_of_term c with
 	  | Var id -> id
 	  | _ ->
-       error "arbitrary substitution of references not implemented")
+       error "Arbitrary substitution of references not implemented.")
      ctxt)
 
 let idopt_of_name = function 
@@ -973,7 +973,7 @@ and raw_of_eqn env constr construct_nargs branch =
             buildrec new_ids (pat::patlist) new_env (n-1) b
 
 	| _ ->
-	    error "Unsupported branch in case-analysis while printing pattern"
+	    error "Unsupported branch in case-analysis while printing pattern."
   in 
   buildrec [] [] env construct_nargs branch
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6fc65e9fb..d802770f0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -99,7 +99,8 @@ let explain_bad_explicitation_number n po =
       str "Bad explicitation name: found " ++ pr_id id ++ 
       str" but was expecting " ++ s
 
-let explain_internalisation_error = function
+let explain_internalisation_error e =
+  let pp = match e with
   | VariableCapture id -> explain_variable_capture id
   | WrongExplicitImplicit -> explain_wrong_explicit_implicit
   | IllegalMetavariable -> explain_illegal_metavariable
@@ -107,16 +108,17 @@ let explain_internalisation_error = function
   | UnboundFixName (iscofix,id) -> explain_unbound_fix_name iscofix id
   | NonLinearPattern id -> explain_non_linear_pattern id
   | BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
-  | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po
+  | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in
+  pp ++ str "."
 
 let error_unbound_patvar loc n =
   user_err_loc
     (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ 
-      str " is unbound")
+      str " is unbound.")
 
 let error_bad_inductive_type loc =
   user_err_loc (loc,"",str 
-    "This should be an inductive type applied to names or \"_\"")
+    "This should be an inductive type applied to names or \"_\".")
 
 let error_inductive_parameter_not_implicit loc =
   user_err_loc (loc,"", str
@@ -180,7 +182,7 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
     make_current_scope (Option.get !idscopes)
     <> make_current_scope (scopt,scopes) then
       user_err_loc (loc,"set_var_scope",
-      pr_id id ++ str " already occurs in a different scope")
+      pr_id id ++ str " already occurs in a different scope.")
   else
     idscopes := Some (scopt,scopes)
 
@@ -300,7 +302,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
   try
     match List.assoc id unbndltacvars with
       | None -> user_err_loc (loc,"intern_var",
-	  str "variable " ++ pr_id id ++ str " should be bound to a term")
+	  str "variable " ++ pr_id id ++ str " should be bound to a term.")
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
   with Not_found ->
   (* Is [id] a goal or section variable *)
@@ -319,14 +321,14 @@ let find_appl_head_data (_,_,_,(_,impls)) = function
   | x -> x,[],[],[]
 
 let error_not_enough_arguments loc =
-  user_err_loc (loc,"",str "Abbreviation is not applied enough")
+  user_err_loc (loc,"",str "Abbreviation is not applied enough.")
 
 let check_no_explicitation l =
   let l = List.filter (fun (a,b) -> b <> None) l in
   if l <> [] then
     let loc = fst (Option.get (snd (List.hd l))) in
     user_err_loc
-      (loc,"",str"Unexpected explicitation of the argument of an abbreviation")
+     (loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
 
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid loc qid intern env args =
@@ -436,7 +438,7 @@ let check_number_of_pattern loc n l =
 let check_or_pat_variables loc ids idsl =
   if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then
     user_err_loc (loc, "", str 
-    "The components of this disjunctive pattern must bind the same variables")
+    "The components of this disjunctive pattern must bind the same variables.")
 
 let check_constructor_length env loc cstr pl pl0 =
   let n = List.length pl + List.length pl0 in
@@ -463,7 +465,7 @@ let message_redundant_alias (id1,id2) =
 (* Expanding notations *)
 
 let error_invalid_pattern_notation loc =
-  user_err_loc (loc,"",str "Invalid notation for pattern")
+  user_err_loc (loc,"",str "Invalid notation for pattern.")
 
 let chop_aconstr_constructor loc (ind,k) args =
   let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
@@ -671,9 +673,9 @@ let locate_if_isevar loc na = function
 
 let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) =
   if List.mem id indnames then
-    errorlabstrm "" (str "A parameter or name of an inductive type " ++
-    pr_id id ++ str " must not be used as a bound variable in the type \
-of its constructor")
+    errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++
+    pr_id id ++ strbrk " must not be used as a bound variable in the type \
+of its constructor.")
 
 let push_name_env lvar (ids,tmpsc,scopes as env) = function
   | Anonymous -> env 
@@ -734,11 +736,11 @@ let check_projection isproj nargs r =
       (try
 	let n = Recordops.find_projection_nparams ref + 1 in
 	if nargs <> n then
-	  user_err_loc (loc,"",str "Projection has not the right number of explicit parameters");
+	  user_err_loc (loc,"",str "Projection has not the right number of explicit parameters.");
       with Not_found -> 
 	user_err_loc
-	(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection"))
-  | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection")
+	(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection."))
+  | _, Some _ -> user_err_loc (loc_of_rawconstr r, "", str "Not a projection.")
   | _, None -> ()
 
 let get_implicit_name n imps =
@@ -763,10 +765,11 @@ let extract_explicit_arg imps args =
 	  let id = match pos with
 	  | ExplByName id ->
 	      if not (exists_implicit_name id imps) then
-		user_err_loc (loc,"",str "Wrong argument name: " ++ pr_id id);
+		user_err_loc
+		  (loc,"",str "Wrong argument name: " ++ pr_id id ++ str ".");
 	      if List.mem_assoc id eargs then
 		user_err_loc (loc,"",str "Argument name " ++ pr_id id
-		++ str " occurs more than once");
+		++ str " occurs more than once.");
 	      id
 	  | ExplByPos (p,_id) ->
 	      let id =
@@ -775,11 +778,12 @@ let extract_explicit_arg imps args =
 		  if not (is_status_implicit imp) then failwith "imp";
 		  name_of_implicit imp
 		with Failure _ (* "nth" | "imp" *) ->
-		  user_err_loc (loc,"",str"Wrong argument position: " ++ int p)
+		  user_err_loc
+		    (loc,"",str"Wrong argument position: " ++ int p ++ str ".")
 	      in
 	      if List.mem_assoc id eargs then
 		user_err_loc (loc,"",str"Argument at position " ++ int p ++
-		  str " is mentioned more than once");
+		  str " is mentioned more than once.");
 	      id in
 	  ((id,(loc,a))::eargs,rargs)
   in aux args
@@ -1003,7 +1007,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	let nal = List.map (function
 	  | RHole loc -> Anonymous
 	  | RVar (_,id) -> Name id
-	  | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
+	  | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in
 	let parnal,realnal = list_chop nparams nal in
 	if List.exists ((<>) Anonymous) parnal then
 	  error_inductive_parameter_not_implicit loc;
@@ -1075,7 +1079,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	  if eargs <> [] then 
 	    (let (id,(loc,_)) = List.hd eargs in
 	       user_err_loc (loc,"",str "Not enough non implicit
-	    arguments to accept the argument bound to " ++ pr_id id));
+	    arguments to accept the argument bound to " ++ 
+		 pr_id id ++ str"."));
 	  []
       | ([], rargs) ->
 	  assert (eargs = []);
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index ecc48dfe2..845707f9e 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -70,7 +70,7 @@ let check_required_library d =
      (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m)
 *)
 (* or failing ...*)
-    error ("Library "^(string_of_dirpath dir)^" has to be required first")
+    error ("Library "^(string_of_dirpath dir)^" has to be required first.")
 
 (************************************************************************)
 (* Specific Coq objects *)
diff --git a/interp/notation.ml b/interp/notation.ml
index bafce17af..164423ead 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -78,7 +78,7 @@ let declare_scope scope =
 
 let find_scope scope =
   try Gmap.find scope !scope_map
-  with Not_found -> error ("Scope "^scope^" is not declared")
+  with Not_found -> error ("Scope "^scope^" is not declared.")
 
 let check_scope sc = let _ = find_scope sc in ()
 
@@ -159,7 +159,7 @@ let find_delimiters_scope loc key =
   try Gmap.find key !delimiters_map
   with Not_found -> 
     user_err_loc 
-    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key))
+    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key^"."))
 
 (* Uninterpretation tables *)
 
@@ -251,7 +251,7 @@ let check_required_module loc sc (sp,d) =
   with Not_found ->
     user_err_loc (loc,"prim_token_interpreter",
     str ("Cannot interpret in "^sc^" without requiring first module "
-    ^(list_last d)))
+    ^(list_last d)^"."))
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
@@ -348,7 +348,7 @@ let interp_prim_token_gen g loc p local_scopes =
     user_err_loc (loc,"interp_prim_token",
     (match p with
       | Numeral n -> str "No interpretation for numeral " ++ pr_bigint n
-      | String s -> str "No interpretation for string " ++ qs s))
+      | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
 let interp_prim_token =
   interp_prim_token_gen (fun x -> x)
@@ -361,7 +361,7 @@ let rec interp_notation loc ntn local_scopes =
   try find_interpretation (find_notation ntn) scopes
   with Not_found ->
     user_err_loc
-    (loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
+    (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
 
 let uninterp_notations c =
   Gmapl.find (rawconstr_key c) !notations_key_table
@@ -625,12 +625,12 @@ let global_reference_of_notation test (ntn,(sc,c,_)) =
   | _ -> None
 
 let error_ambiguous_notation loc _ntn =
-  user_err_loc (loc,"",str "Ambiguous notation")
+  user_err_loc (loc,"",str "Ambiguous notation.")
 
 let error_notation_not_reference loc ntn =
   user_err_loc (loc,"",
     str "Unable to interpret " ++ quote (str ntn) ++
-    str " as a reference")
+    str " as a reference.")
 
 let interp_notation_as_global_reference loc test ntn =
   let ntns = browse_notation true ntn !scope_map in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 8ded0a35b..c684c6adb 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -150,7 +150,7 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
     | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
   | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
       | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
-      -> error "Unsupported construction in recursive notations"
+      -> error "Unsupported construction in recursive notations."
   | (RRef _ | RVar _ | RApp _ | RLambda _ | RProd _ | RHole _ | RSort _), _
       -> false
 
@@ -168,13 +168,13 @@ let discriminate_patterns foundvars nl l1 l2 =
   | _ -> compare_rawconstr (aux (n+1)) c1 c2 in
   let l = list_map2_i aux 0 l1 l2 in
   if not (List.for_all ((=) true) l) then
-    error "Both ends of the recursive pattern differ";
+    error "Both ends of the recursive pattern differ.";
   match !diff with
-    | None ->  error "Both ends of the recursive pattern are the same"
+    | None ->  error "Both ends of the recursive pattern are the same."
     | Some (x,y,_ as discr) ->
 	List.iter (fun id ->
           if List.mem id !foundvars
-          then error "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part";
+          then errorlabstrm "" (strbrk "Variables used in the recursive part of a pattern are not allowed to occur outside of the recursive part.");
           foundvars := id::!foundvars) [x;y];
 	discr
 
@@ -212,7 +212,7 @@ let aconstr_and_vars_of_rawconstr a =
       Array.iter (fun id -> found := id::!found) idl;
       let dll = Array.map (List.map (fun (na,bk,oc,b) -> 
 	 if bk <> Explicit then 
-	   error "Binders marked as implicit not allowed in notations";
+	   error "Binders marked as implicit not allowed in notations.";
 	 add_name found na; (na,Option.map aux oc,aux b))) dll in
       ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
   | RCast (_,c,k) -> ACast (aux c, 
@@ -223,17 +223,17 @@ let aconstr_and_vars_of_rawconstr a =
   | RRef (_,r) -> ARef r
   | RPatVar (_,(_,n)) -> APatVar n
   | RDynamic _ | REvar _ ->
-      error "Existential variables not allowed in notations"
+      error "Existential variables not allowed in notations."
 
   (* Recognizing recursive notations *)
   and terminator_of_pat f1 ll1 lr1 = function
   | RApp (loc,f2,l2) ->
-      if not (eq_rawconstr f1 f2) then error
-	"Cannot recognize the same head to both ends of the recursive pattern";
+      if not (eq_rawconstr f1 f2) then errorlabstrm ""
+	(strbrk "Cannot recognize the same head to both ends of the recursive pattern.");
       let nl = List.length ll1 in
       let nr = List.length lr1 in
       if List.length l2 <> nl + nr + 1 then
-	error "Both ends of the recursive pattern have different lengths";
+	error "Both ends of the recursive pattern have different lengths.";
       let ll2,l2' = list_chop nl l2 in
       let t = List.hd l2' and lr2 = List.tl l2' in
       let x,y,order = discriminate_patterns found nl (ll1@lr1) (ll2@lr2) in
@@ -241,8 +241,8 @@ let aconstr_and_vars_of_rawconstr a =
         if order then RApp (loc,f2,ll2@RVar (loc,ldots_var)::lr2)
         else RApp (loc,f1,ll1@RVar (loc,ldots_var)::lr1) in
       (if order then y else x),(if order then x else y), aux iter, aux t, order
-  | _ -> error "One end of the recursive pattern is not an application"
-    
+  | _ -> error "One end of the recursive pattern is not an application."
+
   and make_aconstr_list f args =
     let rec find_patterns acc = function
       | RApp(_,RVar (_,a),[c]) :: l when a = ldots_var ->
@@ -250,7 +250,7 @@ let aconstr_and_vars_of_rawconstr a =
 	  let x,y,iter,term,lassoc = terminator_of_pat f (List.rev acc) l c in
 	  AList (x,y,iter,term,lassoc)
       | a::l -> find_patterns (a::acc) l
-      | [] -> error "Ill-formed recursive notation"
+      | [] -> error "Ill-formed recursive notation."
     in find_patterns [] args
 
   in
@@ -262,7 +262,7 @@ let aconstr_of_rawconstr vars a =
   let a,foundvars = aconstr_and_vars_of_rawconstr a in
   let check_type x =
     if not (List.mem x foundvars) then
-      error ((string_of_id x)^" is unbound in the right-hand-side") in
+      error ((string_of_id x)^" is unbound in the right-hand-side.") in
   List.iter check_type vars;
   a
 
@@ -853,7 +853,7 @@ let coerce_to_id = function
   | CRef (Ident (loc,id)) -> (loc,id)
   | a -> user_err_loc
         (constr_loc a,"coerce_to_id",
-         str "This expression should be a simple identifier")
+         str "This expression should be a simple identifier.")
 
 (* Used in correctness and interface *)