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

16 files changed, 56 insertions, 56 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 52c8ca419..3839561bf 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -114,8 +114,8 @@ let force_name =
 
 open Pp
 
-let mssg_may_need_inversion () =
-  str "Found a matching with no clauses on a term unknown to have an empty inductive type"
+let msg_may_need_inversion () =
+  strbrk "Found a matching with no clauses on a term unknown to have an empty inductive type."
 
 (* Utils *)
 let make_anonymous_patvars n =
@@ -535,7 +535,7 @@ let set_used_pattern eqn = eqn.used := true
 
 let extract_rhs pb =
   match pb.mat with 
-    | [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion())
+    | [] -> errorlabstrm "build_leaf" (msg_may_need_inversion())
     | eqn::_ ->
 	set_used_pattern eqn;
         eqn.rhs
@@ -1654,7 +1654,7 @@ let extract_arity_signature env0 tomatchl tmsign =
 	    | None -> [na,Option.map (lift n) bo,lift n typ]
 	    | Some (loc,_,_,_) -> 
  	    user_err_loc (loc,"",
-	    str "Unexpected type annotation for a term of non inductive type"))
+	    str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = lift_inductive_family n indf in
 	  let (ind,params) = dest_ind_family indf' in
@@ -1663,7 +1663,7 @@ let extract_arity_signature env0 tomatchl tmsign =
 	    match t with
 	      | Some (loc,ind',nparams,realnal) ->
 		  if ind <> ind' then
-		    user_err_loc (loc,"",str "Wrong inductive type");
+		    user_err_loc (loc,"",str "Wrong inductive type.");
 		  if List.length params <> nparams
 		    or nrealargs <> List.length realnal then
 		      anomaly "Ill-formed 'in' clause in cases";
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 0d7e3d611..0ffaed371 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -376,7 +376,7 @@ let coercion_of_reference r =
   let ref = Nametab.global r in
   if not (coercion_exists ref) then
     errorlabstrm "try_add_coercion" 
-      (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion");
+      (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion.");
   ref
 
 module CoercionPrinting =
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index c91580044..732ff1e69 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -377,11 +377,11 @@ let check_bindings bl =
     | NamedHyp s :: _ -> 
 	errorlabstrm ""
 	  (str "The variable " ++ pr_id s ++ 
-	   str " occurs more than once in binding list");
+	   str " occurs more than once in binding list.");
     | AnonHyp n :: _ ->
 	errorlabstrm ""
 	  (str "The position " ++ int n ++
-	   str " occurs more than once in binding list")
+	   str " occurs more than once in binding list.")
     | [] -> ()
 
 let meta_of_binder clause loc mvs = function
@@ -389,17 +389,17 @@ let meta_of_binder clause loc mvs = function
   | AnonHyp n ->
       try List.nth mvs (n-1)
       with (Failure _|Invalid_argument _) ->
-        errorlabstrm "" (str "No such binder")
+        errorlabstrm "" (str "No such binder.")
 
 let error_already_defined b =
   match b with
     | NamedHyp id ->
         errorlabstrm ""
           (str "Binder name \"" ++ pr_id id ++
-           str"\" already defined with incompatible value")
+           str"\" already defined with incompatible value.")
     | AnonHyp n ->
         anomalylabstrm ""
-          (str "Position " ++ int n ++ str" already defined")
+          (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
   if isMeta (fst (whd_stack u)) then
@@ -440,7 +440,7 @@ let clenv_constrain_last_binding c clenv =
   let all_mvs = collect_metas clenv.templval.rebus in
   let k =
     try list_last all_mvs 
-    with Failure _ -> error "clenv_constrain_with_bindings" in
+    with Failure _ -> anomaly "clenv_constrain_with_bindings" in
   clenv_assign_binding clenv k (Evd.empty,c)
 
 let clenv_constrain_dep_args hyps_only bl clenv =
@@ -451,8 +451,9 @@ let clenv_constrain_dep_args hyps_only bl clenv =
     if List.length occlist = List.length bl then
       List.fold_left2 clenv_assign_binding clenv occlist bl
     else 
-      error ("Not the right number of missing arguments (expected "
-	     ^(string_of_int (List.length occlist))^")")
+      errorlabstrm "" 
+	(strbrk "Not the right number of missing arguments (expected " ++
+	 int (List.length occlist) ++ str ").")
 
 (****************************************************************)
 (* Clausal environment for an application *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8d8a9950e..6854a4a7c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -49,14 +49,14 @@ let encode_bool r =
   let (_,lc as x) = encode_inductive r in
   if not (has_two_constructors lc) then
     user_err_loc (loc_of_reference r,"encode_if",
-      str "This type has not exactly two constructors");
+      str "This type has not exactly two constructors.");
   x
 
 let encode_tuple r =
   let (_,lc as x) = encode_inductive r in
   if not (isomorphic_to_tuple lc) then
     user_err_loc (loc_of_reference r,"encode_tuple",
-      str "This type cannot be seen as a tuple type");
+      str "This type cannot be seen as a tuple type.");
   x
 
 module PrintingCasesMake =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 1463901a5..cd09691d0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -505,7 +505,7 @@ let choose_less_dependent_instance evk evd term args =
   let evi = Evd.find (evars_of evd) evk in
   let subst = make_pure_subst evi args in
   let subst' = List.filter (fun (id,c) -> c = term) subst in
-  if subst' = [] then error "Too complex unification problem" else
+  if subst' = [] then error "Too complex unification problem." else
   Evd.evar_define evk (mkVar (fst (List.hd subst'))) evd
 
 let apply_conversion_problem_heuristic env evd pbty t1 t2 =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 870debaa7..2f2665bbc 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -451,8 +451,9 @@ let clear_hyps_in_evi evdref hyps concl ids =
 	    None -> None
 	  | Some b -> Some (check_and_clear_in_constr evdref b ids EvkSet.empty)),
 	check_and_clear_in_constr evdref c ids EvkSet.empty)
-      with Dependency_error id' -> error (string_of_id id' ^ " is used in hypothesis "
-					   ^ string_of_id id) 
+      with Dependency_error id' ->
+	errorlabstrm "" (pr_id id' ++ strbrk " is used in hypothesis "
+					   ++ pr_id id ++ str ".")
     in
     let check_value vk =
       match !vk with
@@ -883,7 +884,7 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
 and evar_define env (evk,_ as ev) rhs evd =
   try
     let (evd',body) = invert_definition env evd ev rhs in
-    if occur_meta body then error "Meta cannot occur in evar body";
+    if occur_meta body then error "Meta cannot occur in evar body.";
     (* invert_definition may have instantiate some evars of rhs with evk *)
     (* so we recheck acyclicity *)
     if occur_evar evk body then error_occur_check env (evars_of evd) evk body;
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 166114ab6..ecc63ce94 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -598,13 +598,13 @@ let meta_with_name evd id =
   match mvnodef, mvl with
     | _,[]  -> 
 	errorlabstrm "Evd.meta_with_name"
-          (str"No such bound variable " ++ pr_id id)
+          (str"No such bound variable " ++ pr_id id ++ str".")
     | ([n],_|_,[n]) -> 
 	n
     | _  -> 
 	errorlabstrm "Evd.meta_with_name"
           (str "Binder name \"" ++ pr_id id ++
-           str"\" occurs more than once in clause")
+           strbrk "\" occurs more than once in clause.")
 
 
 let meta_merge evd1 evd2 =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 37d60e470..ffbc9debc 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -591,12 +591,10 @@ let lookup_eliminator ind_sp s =
   try constr_of_global (Nametab.locate (make_short_qualid id))
   with Not_found ->
     errorlabstrm "default_elim"
-      (str "Cannot find the elimination combinator " ++
-       pr_id id ++ spc () ++
-       str "The elimination of the inductive definition " ++
-       pr_id id ++ spc () ++ str "on sort " ++ 
-       spc () ++ pr_sort_family s ++
-       str " is probably not allowed")
+      (strbrk "Cannot find the elimination combinator " ++
+       pr_id id ++ strbrk ", the elimination of the inductive definition " ++
+       pr_id id ++ strbrk " on sort " ++ pr_sort_family s ++
+       strbrk " is probably not allowed.")
 
 
 (*  let env = Global.env() in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 66f345643..79d9e381e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -87,7 +87,7 @@ let mis_nf_constructor_type (ind,mib,mip) j =
   and ntypes = mib.mind_ntypes
   and nconstr = Array.length mip.mind_consnames in
   let make_Ik k = mkInd ((fst ind),ntypes-k-1) in 
-  if j > nconstr then error "Not enough constructors in the type";
+  if j > nconstr then error "Not enough constructors in the type.";
   substl (list_tabulate make_Ik ntypes) specif.(j-1)
 
 (* Arity of constructors excluding parameters and local defs *)
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 6b3b4e175..9a3130605 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -110,7 +110,7 @@ let matches_core convert allow_partial_app pat c =
 	    List.map
 	      (function
 		 | PRel n -> n
-		 | _ -> error "Only bound indices allowed in second order pattern matching")
+		 | _ -> error "Only bound indices allowed in second order pattern matching.")
 	      args in
 	  let frels = Intset.elements (free_rels cT) in
 	  if list_subset frels relargs then
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 05af1652e..ba53d127e 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -133,7 +133,7 @@ let map_pattern f = map_pattern_with_binders (fun () -> ()) (fun () -> f) ()
 
 let rec instantiate_pattern lvar = function
   | PVar id as x -> (try Lazy.force(List.assoc id lvar) with Not_found -> x)
-  | (PFix _ | PCoFix _) -> error ("Not instantiable pattern")
+  | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
   | c -> map_pattern (instantiate_pattern lvar) c
 
 let rec liftn_pattern k n = function
@@ -264,7 +264,7 @@ let rec pat_of_raw metas vars = function
              
   | r ->
       let loc = loc_of_rawconstr r in
-      user_err_loc (loc,"pattern_of_rawconstr", Pp.str "Pattern not supported")
+      user_err_loc (loc,"pattern_of_rawconstr", Pp.str"Non supported pattern.")
 
 and pat_of_raw_branch loc metas vars ind brs i =
   let bri = List.filter
@@ -272,23 +272,23 @@ and pat_of_raw_branch loc metas vars ind brs i =
         (_,_,[PatCstr(_,c,lv,Anonymous)],_) -> snd c = i+1
       | (loc,_,_,_) ->
           user_err_loc (loc,"pattern_of_rawconstr",
-                        Pp.str "Not supported pattern")) brs in
+                        Pp.str "Non supported pattern.")) brs in
   match bri with
     | [(_,_,[PatCstr(_,(indsp,_),lv,_)],br)] ->
 	if ind <> None & ind <> Some indsp then
           user_err_loc (loc,"pattern_of_rawconstr",
-            Pp.str "All constructors must be in the same inductive type");
+            Pp.str "All constructors must be in the same inductive type.");
         let lna =
           List.map
             (function PatVar(_,na) -> na
               | PatCstr(loc,_,_,_) ->
                   user_err_loc (loc,"pattern_of_rawconstr",
-                                Pp.str "Not supported pattern")) lv in
+                                Pp.str "Non supported pattern.")) lv in
         let vars' = List.rev lna @ vars in 
 	List.length lv, rev_it_mkPLambda lna (pat_of_raw metas vars' br)
     | _ -> user_err_loc (loc,"pattern_of_rawconstr",
                          str "No unique branch for " ++ int (i+1) ++
-                         str"-th constructor")
+                         str"-th constructor.")
 
 let pattern_of_rawconstr c =
   let metas = ref [] in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 17c7efb45..08ecae12e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -66,7 +66,7 @@ let search_guard loc env possible_indexes fixdefs =
 	    try check_fix env fix; raise (Found indexes) 
 	    with TypeError _ -> ())
 	 (list_combinations possible_indexes); 
-       let errmsg = "cannot guess decreasing argument of fix" in 
+       let errmsg = "Cannot guess decreasing argument of fix." in 
        if loc = dummy_loc then error errmsg else 
 	 user_err_loc (loc,"search_guard", Pp.str errmsg)
      with Found indexes -> indexes)
@@ -244,7 +244,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     try (* To build a nicer ltac error message *)
       match List.assoc id unbndltacvars with
       | None -> user_err_loc (loc,"",
-	  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 ->
       error_var_not_found_loc loc id
@@ -461,10 +461,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	in
 	let cstrs = get_constructors env indf in
 	  if Array.length cstrs <> 1 then
-            user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
+            user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor.");
 	  let cs = cstrs.(0) in
 	    if List.length nal <> cs.cs_nargs then
-              user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
+              user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables.");
 	    let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
               (List.rev nal) cs.cs_args in
 	    let env_f = push_rels fsign env in
@@ -527,7 +527,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let cstrs = get_constructors env indf in 
 	  if Array.length cstrs <> 2 then
             user_err_loc (loc,"",
-			  str "If is only for inductive types with two constructors");
+			  str "If is only for inductive types with two constructors.");
 
 	  let arsgn = 
 	    let arsgn,_ = get_arity env indf in
@@ -615,7 +615,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	    j
 	      (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
 	else
-	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))
+	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic."))
 
   (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
   and pretype_type valcon env evdref lvar = function
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 7dbbf9933..100109652 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -217,7 +217,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 
 let error_not_structure ref =
   errorlabstrm "object_declare"
-    (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object")
+    (Nameops.pr_id (id_of_global ref) ++ str" is not a structure object.")
 
 let check_and_decompose_canonical_structure ref =
   let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 055d2e51b..12594dd6d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -773,7 +773,7 @@ let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
   match kind_of_term c with
     | Sort s -> l,s
-    | _ -> error "not an arity"
+    | _ -> invalid_arg "splay_arity"
 
 let sort_of_arity env c = snd (splay_arity env Evd.empty c)
 
@@ -783,7 +783,7 @@ let decomp_n_prod env sigma n =
       | Prod (n,a,c0) ->
 	  decrec (push_rel (n,None,a) env)
 	    (m-1) (Sign.add_rel_decl (n,None,a) ln) c0
-      | _                      -> error "decomp_n_prod: Not enough products"
+      | _                      -> invalid_arg "decomp_n_prod"
   in 
   decrec env n Sign.empty_rel_context
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 47bc132ac..0dd94d813 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -543,7 +543,7 @@ let try_red_product env sigma c =
 
 let red_product env sigma c = 
   try try_red_product env sigma c
-  with Redelimination -> error "Not reducible"
+  with Redelimination -> error "Not reducible."
 
 (*
 (* This old version of hnf uses betadeltaiota instead of itself (resp 
@@ -698,7 +698,7 @@ let unfold env sigma name =
   if is_evaluable env name then
     clos_norm_flags (unfold_red name) env sigma
   else
-    error (string_of_evaluable_ref env name^" is opaque")
+    error (string_of_evaluable_ref env name^" is opaque.")
 
 (* [unfoldoccs : (readable_constraints -> (int list * section_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
@@ -709,7 +709,7 @@ let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c =
   else
     let (nbocc,uc) = substlin env name 1 plocs c in
     if nbocc = 1 then 
-      error ((string_of_evaluable_ref env name)^" does not occur");
+      error ((string_of_evaluable_ref env name)^" does not occur.");
     let rest = List.filter (fun o -> o >= nbocc) locs in
     if rest <> [] then error_invalid_occurrence rest;
     nf_betaiota uc
@@ -722,7 +722,7 @@ let unfoldn loccname env sigma c =
 let fold_one_com com env sigma c =
   let rcom =
     try red_product env sigma com
-    with Redelimination -> error "Not reducible" in
+    with Redelimination -> error "Not reducible." in
   (* Reason first on the beta-iota-zeta normal form of the constant as
      unfold produces it, so that the "unfold f; fold f" configuration works
      to refold fix expressions *)
@@ -757,7 +757,7 @@ let compute = cbv_betadeltaiota
 let abstract_scheme env sigma (locc,a) c =
   let ta = Retyping.get_type_of env sigma a in
   let na = named_hd env ta Anonymous in
-  if occur_meta ta then error "cannot find a type for the generalisation";
+  if occur_meta ta then error "Cannot find a type for the generalisation.";
   if occur_meta a then 
     mkLambda (na,ta,c)
   else 
@@ -785,14 +785,14 @@ let reduce_to_ind_gen allow_product env sigma t =
 	  if allow_product then
 	    elimrec (push_rel (n,None,ty) env) t' ((n,None,ty)::l)
 	  else
-	    errorlabstrm "" (str"Not an inductive definition")
+	    errorlabstrm "" (str"Not an inductive definition.")
       | _ ->
 	  (* Last chance: we allow to bypass the Opaque flag (as it
 	     was partially the case between V5.10 and V8.1 *)
 	  let t' = whd_betadeltaiota env sigma t in
 	  match kind_of_term (fst (decompose_app t')) with
 	    | Ind ind-> (ind, it_mkProd_or_LetIn t' l)
-	    | _ -> errorlabstrm "" (str"Not an inductive product")
+	    | _ -> errorlabstrm "" (str"Not an inductive product.")
   in
   elimrec env t []
 
@@ -843,7 +843,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
     let (mind,t) = reduce_to_ind_gen allow_product env sigma t in
     if IndRef mind <> ref then
       errorlabstrm "" (str "Cannot recognize a statement based on " ++ 
-        Nametab.pr_global_env Idset.empty ref)
+        Nametab.pr_global_env Idset.empty ref ++ str".")
     else
       t
   else
@@ -857,7 +857,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
 	  else 
 	     errorlabstrm "" 
 	       (str "Cannot recognize an atomic statement based on " ++ 
-	        Nametab.pr_global_env Idset.empty ref)
+	        Nametab.pr_global_env Idset.empty ref ++ str".")
       | _ ->
 	  try 
 	    if global_of_constr c = ref 
@@ -870,7 +870,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
           with NotStepReducible ->
 	    errorlabstrm ""
 	      (str "Cannot recognize a statement based on " ++ 
-	       Nametab.pr_global_env Idset.empty ref)
+	       Nametab.pr_global_env Idset.empty ref ++ str".")
   in
   elimrec env t []
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 4246f0daa..22090d88c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -639,7 +639,7 @@ let error_invalid_occurrence l =
   let l = list_uniquize (List.sort Pervasives.compare l) in
   errorlabstrm ""
     (str ("Invalid occurrence " ^ plural (List.length l) "number" ^": ") ++ 
-     prlist_with_sep spc int l)
+     prlist_with_sep spc int l ++ str ".")
 
 let subst_term_occ_gen (nowhere_except_in,locs) occ c t =
   let maxocc = List.fold_right max locs 0 in