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

20 files changed, 207 insertions, 203 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index dfc9a6ad20..1c3e2ce086 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -220,7 +220,7 @@ let rec nb_hyp c = match kind_of_term c with
 
 let try_head_pattern c = 
   try head_pattern_bound c
-  with BoundPattern -> error "Bound head variable"
+  with BoundPattern -> error "Bound head variable."
 
 let dummy_goal = 
   {it = make_evar empty_named_context_val mkProp;
@@ -279,8 +279,8 @@ let make_resolves env sigma flags pri c =
   if ents = [] then
     errorlabstrm "Hint" 
       (pr_lconstr c ++ spc() ++ 
-        (if fst flags then str"cannot be used as a hint"
-	else str "can be used as a hint only for eauto"));
+        (if fst flags then str"cannot be used as a hint."
+	else str "can be used as a hint only for eauto."));
   ents
 
 (* used to add an hypothesis to the local hint database *)
@@ -438,7 +438,7 @@ let add_extern pri (patmetas,pat) tacast local dbname =
   match (list_subtract tacmetas patmetas) with
     | i::_ ->
 	errorlabstrm "add_extern" 
-	  (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound")
+	  (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.")
     | []  ->
 	Lib.add_anonymous_leaf
 	  (inAutoHint(local,dbname, UpdateDB [make_extern pri pat tacast]))
@@ -476,7 +476,7 @@ let add_hints local dbnames0 h =
          | _ -> 
            errorlabstrm "evalref_of_ref"
             (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++
-             str "to an evaluable reference")
+             str "to an evaluable reference.")
         in
 	  if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr;
 	 (gr,r') in
@@ -571,6 +571,9 @@ let fmt_hint_term cl =
 	 hov 0 (prlist fmt_hints_db valid_dbs))
   with Bound | Match_failure _ | Failure _ -> 
     (str "No hint applicable for current goal")
+
+let error_no_such_hint_database x =
+  error ("No such Hint database: "^x^".")
 	  
 let print_hint_term cl = ppnl (fmt_hint_term cl)
 
@@ -597,13 +600,13 @@ let print_hint_db_by_name dbname =
   try 
     let db = searchtable_map dbname in print_hint_db db
   with Not_found -> 
-    error (dbname^" : No such Hint database")
+    error_no_such_hint_database dbname
   
 (* displays all the hints of all databases *)
 let print_searchtable () =
   Hintdbmap.iter
     (fun name db ->
-       msg (str "In the database " ++ str name ++ fnl ());
+       msg (str "In the database " ++ str name ++ str ":" ++ fnl ());
        print_hint_db db)
     !searchtable
 
@@ -774,7 +777,7 @@ let trivial lems dbnames gl =
 	 try 
 	   searchtable_map x
 	 with Not_found -> 
-	   error ("trivial: "^x^": No such Hint database"))
+	   error_no_such_hint_database x)
       ("core"::dbnames) 
   in
   tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl 
@@ -813,7 +816,7 @@ let decomp_unary_term c gls =
   if Hipattern.is_conjunction hd then 
     simplest_case c gls 
   else 
-    errorlabstrm "Auto.decomp_unary_term" (str "not a unary type") 
+    errorlabstrm "Auto.decomp_unary_term" (str "Not a unary type.")
 
 let decomp_empty_term c gls = 
   let typc = pf_type_of gls c in 
@@ -821,7 +824,7 @@ let decomp_empty_term c gls =
   if Hipattern.is_empty_type hd then 
     simplest_case c gls 
   else 
-    errorlabstrm "Auto.decomp_empty_term" (str "not an empty type") 
+    errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.")
 
 
 (* decomp is an natural number giving an indication on decomposition 
@@ -877,7 +880,7 @@ let delta_auto mod_delta n lems dbnames gl =
 	 try 
 	   searchtable_map x
 	 with Not_found -> 
-	   error ("auto: "^x^": No such Hint database"))
+	   error_no_such_hint_database x)
       ("core"::dbnames) 
   in
   let hyps = pf_hyps gl in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 3be1e45dee..68c61bca04 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -56,7 +56,7 @@ let print_rewrite_hintdb bas =
  with
   Not_found -> 
    errorlabstrm "AutoRewrite" 
-     (str ("Rewriting base "^(bas)^" does not exist"))
+     (str ("Rewriting base "^(bas)^" does not exist."))
 
 type raw_rew_rule = constr * bool * raw_tactic_expr
 
@@ -67,7 +67,7 @@ let one_base general_rewrite_maybe_in tac_main bas =
       Stringmap.find bas !rewtab
     with Not_found ->
       errorlabstrm "AutoRewrite"
-        (str ("Rewriting base "^(bas)^" does not exist"))
+        (str ("Rewriting base "^(bas)^" does not exist."))
   in
   let lrul = List.map (fun (c,_,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in
     tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
@@ -99,7 +99,7 @@ let autorewrite_multi_in idl tac_main lbas : tactic =
      match (Environ.named_context_of_val gl.Evd.it.Evd.evar_hyps) with
         (last_hyp_id,_,_)::_ -> last_hyp_id
       | _ -> (* even the hypothesis id is missing *)
-             error ("No such hypothesis : " ^ (string_of_id !id))
+             error ("No such hypothesis: " ^ (string_of_id !id) ^".")
     in
     let gl' = general_rewrite_in dir all_occurrences !id cstr false gl in
     let gls = (fst gl').Evd.it in
@@ -140,7 +140,7 @@ let gen_auto_multi_rewrite tac_main lbas cl =
   if cl.concl_occs <> all_occurrences_expr &
      cl.concl_occs <> no_occurrences_expr
   then 
-    error "The \"at\" syntax isn't available yet for the autorewrite tactic"
+    error "The \"at\" syntax isn't available yet for the autorewrite tactic."
   else 
     let compose_tac t1 t2 = 
       match cl.onhyps with 
@@ -170,8 +170,7 @@ let auto_multi_rewrite_with tac_main lbas cl gl =
 	gen_auto_multi_rewrite tac_main  lbas cl gl
     | _ -> 
 	    Util.errorlabstrm "autorewrite" 
-	      (str "autorewrite .. in .. using can only be used either with a unique hypothesis or" ++
-		 str " on the conclusion")
+	      (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
 
 
 (* Functions necessary to the library object declaration *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6312cefc18..700ce5895a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -49,7 +49,7 @@ let check_imported_library d =
   let d' = List.map id_of_string d in
   let dir = make_dirpath (List.rev d') in
   if not (Library.library_is_loaded dir) then
-    error ("Library "^(list_last d)^" has to be imported first")
+    error ("Library "^(list_last d)^" has to be imported first.")
       
 let classes_dirpath =
   make_dirpath (List.map id_of_string ["Classes";"Coq"])
@@ -354,7 +354,7 @@ let e_breadth_search debug s =
     let tac = 
       if debug then Search.debug_breadth_first else Search.breadth_first 
     in let s = tac s in s.tacres
-  with Not_found -> error "EAuto: breadth first search failed"
+  with Not_found -> error "eauto: breadth first search failed."
 
 let e_search_auto debug (in_depth,p) lems st db_list gls = 
   let sigma = Evd.sig_sig (fst gls) and gls' = Evd.sig_it (fst gls) in
@@ -727,13 +727,13 @@ let decompose_setoid_eqhyp env sigma c left2right =
     | [c1;c2] -> [],(c1, c2)
     | x::y::z ->
 	let l,res = split_last_two (y::z) in x::l, res
-    | _ -> error "The term provided is not an applied relation" in
+    | _ -> error "The term provided is not an applied relation." in
   let others,(c1,c2) = split_last_two args in
   let ty1, ty2 = 
     Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2
   in
     if not (evd_convertible env eqclause.evd ty1 ty2) then
-      error "The term does not end with an applied homogeneous relation"
+      error "The term does not end with an applied homogeneous relation."
     else
       { cl=eqclause; prf=(Clenv.clenv_value eqclause);
 	car=ty1; rel=mkApp (equiv, Array.of_list others);
@@ -1102,7 +1102,7 @@ let occurrences_of = function
   | n::_ as nl when n < 0 -> (false,List.map abs nl)
   | nl -> 
       if List.exists (fun n -> n < 0) nl then
-	error "Illegal negative occurrence number";
+	error "Illegal negative occurrence number.";
       (true,nl)
 
 TACTIC EXTEND class_rewrite
@@ -1609,7 +1609,7 @@ let relation_of_constr c =
     | App (f, args) when Array.length args >= 2 -> 
 	let relargs, args = array_chop (Array.length args - 2) args in
 	  mkApp (f, relargs), args
-    | _ -> error "Not an applied relation"
+    | _ -> error "Not an applied relation."
 
 let is_loaded d =
   let d' = List.map id_of_string d in
@@ -1656,7 +1656,7 @@ let setoid_symmetry_in id gl =
   let rec split_last_two = function
     | [c1;c2] -> [],(c1, c2)
     | x::y::z -> let l,res = split_last_two (y::z) in x::l, res
-    | _ -> error "The term provided is not an equivalence" 
+    | _ -> error "The term provided is not an equivalence."
   in
   let others,(c1,c2) = split_last_two args in
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 535fd6632e..4b48064b31 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -85,7 +85,7 @@ let contradiction_term (c,lbind as cl) gl =
 	  (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) gl
       else
 	raise Not_found
-    with Not_found -> error "Not a contradiction"
+    with Not_found -> error "Not a contradiction."
 
 let contradiction = function
   | None -> tclTHEN intros contradiction_context
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 4eb59a2fb0..a25fcd923b 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 open Util
 open Names
@@ -162,8 +162,8 @@ let decompose_eq env id =
 	App (f,args)->
 	  if eq_constr f _eq && (Array.length args)=3 
 	  then args.(0)
-	  else error "previous step is not an equality"
-      | _ -> error "previous step is not an equality"
+	  else error "Previous step is not an equality."
+      | _ -> error "Previous step is not an equality."
 
 let get_eq_typ info env =
   let typ = decompose_eq env (get_last env) in  
@@ -331,9 +331,9 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
     let expected = mib.Declarations.mind_nparams - num_params in
       if List.length params <> expected then
 	errorlabstrm "suppose it is" 
-	  (str "Wrong number of extra arguments : " ++ 
+	  (str "Wrong number of extra arguments: " ++ 
 	     (if expected = 0 then str "none" else int expected) ++ 
-	     str "expected") in
+	     str "expected.") in
   let app_ind =
     let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in
     let rparams = List.map detype_ground pinfo.per_params in 
@@ -400,7 +400,7 @@ let interp_suffices_clause sigma env (hyps,cot)=
 	  let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in
 	  nhyps,This nc
       | Thesis Plain as th  -> interp_hyps sigma env hyps,th
-      | Thesis (For n) -> error "\"thesis for\" is not applicable here" in
+      | Thesis (For n) -> error "\"thesis for\" is not applicable here." in
   let push_one hyp env0 =
     match hyp with
 	(Hprop st | Hvar st) ->
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 133524ba76..cbb8996f64 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -188,7 +188,7 @@ let close_tactic_mode pts =
     let pts1=  
       try goto_current_focus pts 
       with Not_found -> 
-	error "\"return\" cannot be used outside of Declarative Proof Mode" in
+	error "\"return\" cannot be used outside of Declarative Proof Mode." in
     let pts2 = daimon_subtree pts1 in
     let pts3 = mark_as_done pts2 in 
       goto_current_focus pts3 
@@ -207,18 +207,18 @@ let close_block bt pts =
 	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> 
 	  daimon_subtree (goto_current_focus pts)
       | _, Claim::_ -> 
-	  error "\"end claim\" expected" 
+	  error "\"end claim\" expected."
       | _, Focus_claim::_ -> 
-	  error "\"end focus\" expected" 
+	  error "\"end focus\" expected."
       | _, [] ->
- 	  error "\"end proof\" expected" 
+ 	  error "\"end proof\" expected."
       | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) ->
 	  begin
 	    match et with
-		ET_Case_analysis -> error "\"end cases\" expected"
-	      | ET_Induction ->  error "\"end induction\" expected"
+		ET_Case_analysis -> error "\"end cases\" expected."
+	      | ET_Induction ->  error "\"end induction\" expected."
 	  end
-      | _,_ -> anomaly "lonely suppose on stack"
+      | _,_ -> anomaly "Lonely suppose on stack."
 
 (* utility for suppose / suppose it is *)
 
@@ -284,10 +284,10 @@ let justification tac gls=
       (tclSOLVE [tclTHEN tac assumption]) 
       (fun gls -> 
 	 if get_strictness () then 
-	   error "insufficient justification" 
+	   error "Insufficient justification."
 	 else
 	   begin
-	     msg_warning (str "insufficient justification");  
+	     msg_warning (str "Insufficient justification.");
 	     daimon_tac gls
 	   end) gls
 
@@ -475,7 +475,7 @@ let thus_tac c ctyp submetas gls =
     try
       find_subsubgoal c ctyp 0 submetas gls
     with Not_found -> 
-      error "I could not relate this statement to the thesis" in
+      error "I could not relate this statement to the thesis." in
   if list = [] then
     exact_check proof gls 
   else
@@ -490,7 +490,7 @@ let anon_id_base = id_of_string "__"
 let mk_stat_or_thesis info gls = function  
     This c -> c
   | Thesis (For _ ) -> 
-      error "\"thesis for ...\" is not applicable here" 
+      error "\"thesis for ...\" is not applicable here."
   | Thesis Plain -> pf_concl gls
 
 let just_tac _then cut info gls0 =
@@ -542,12 +542,12 @@ let decompose_eq id gls =
 	  then (args.(0),
 		args.(1), 
 		args.(2)) 
-	  else error "previous step is not an equality"
-      | _ -> error "previous step is not an equality"
+	  else error "Previous step is not an equality."
+      | _ -> error "Previous step is not an equality."
 	  
 let instr_rew _thus rew_side cut gls0 = 
   let last_id = 
-    try get_last (pf_env gls0) with _ -> error "no previous equality" in
+    try get_last (pf_env gls0) with _ -> error "No previous equality." in
   let typ,lhs,rhs = decompose_eq last_id gls0 in  
   let items_tac gls =
     match cut.cut_by with
@@ -730,7 +730,7 @@ let rec consider_match may_intro introduced available expected gls =
   match available,expected with 
       [],[] ->
 	  tclIDTAC gls
-    | _,[] -> error "last statements do not match a complete hypothesis" 
+    | _,[] -> error "Last statements do not match a complete hypothesis."
 	(* should tell which ones *)
     | [],hyps -> 
 	if may_intro then
@@ -740,11 +740,11 @@ let rec consider_match may_intro introduced available expected gls =
 		(intro_mustbe_force id)
 		(consider_match true [] [id] hyps) 
 		(fun _ -> 
-		   error "not enough sub-hypotheses to match statements")
+		   error "Not enough sub-hypotheses to match statements.")
 		gls 
           end 
 	else
-	  error "not enough sub-hypotheses to match statements" 
+	  error "Not enough sub-hypotheses to match statements."
 	    (* should tell which ones *)
     | id::rest_ids,(Hvar st | Hprop st)::rest ->
 	tclIFTHENELSE (convert_hyp (id,None,st.st_it))
@@ -761,7 +761,7 @@ let rec consider_match may_intro introduced available expected gls =
 	    (fun gls -> 
 	       let nhyps =
 		 try conjunction_arity id gls with 
-		     Not_found -> error "matching hypothesis not found" in 
+		     Not_found -> error "Matching hypothesis not found." in 
 		 tclTHENLIST 
 		   [general_case_analysis false (mkVar id,NoBindings);
 		    intron_then nhyps []
@@ -818,7 +818,7 @@ let cast_tac id_or_thesis typ gls =
 	let (_,body,_) = pf_get_hyp gls id in
 	  convert_hyp (id,body,typ) gls
     | Thesis (For _ ) -> 
-	error "\"thesis for ...\" is not applicable here" 
+	error "\"thesis for ...\" is not applicable here."
     | Thesis Plain ->    
           convert_concl typ DEFAULTcast gls
       
@@ -884,7 +884,7 @@ let build_per_info etype casee gls =
     try
       destInd hd 
     with _ -> 
-      error "Case analysis must be done on an inductive object" in
+      error "Case analysis must be done on an inductive object." in
   let mind,oind = Global.lookup_inductive ind in
   let nparams,index =
     match etype with
@@ -1042,7 +1042,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
 		      | Split_patt (_,ind0,_) ->
 			  if (ind <> ind0) then error
 			    (* this can happen with coercions *)
-	                    "Case pattern belongs to wrong inductive type";
+	                    "Case pattern belongs to wrong inductive type.";
 			  let mapi i ati bri =
 			    if i = pred cnum then 
 			      let nargs = 
@@ -1083,12 +1083,12 @@ let thesis_for obj typ per_info env=
   let _ = if ind <> per_info.per_ind then
     errorlabstrm "thesis_for" 
       ((Printer.pr_constr_env env obj) ++ spc () ++ 
-	 str "cannot give an induction hypothesis (wrong inductive type)") in  
+	 str"cannot give an induction hypothesis (wrong inductive type).") in  
   let params,args = list_chop per_info.per_nparams all_args in
   let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
     errorlabstrm "thesis_for" 
       ((Printer.pr_constr_env env obj) ++ spc () ++ 
-	 str "cannot give an induction hypothesis (wrong parameters)") in
+	 str "cannot give an induction hypothesis (wrong parameters).") in
   let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
     compose_prod rc (whd_beta hd2)
 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 7d2ccbe219..80b505a00e 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -246,7 +246,7 @@ let add_destructor_hint local na loc pat pri code =
       | ConclLocation _, _ -> (None, code)
       | _ ->
 	  errorlabstrm "add_destructor_hint"
-          (str "The tactic should be a function of the hypothesis name") end
+          (str "The tactic should be a function of the hypothesis name.") end
   in
   let (_,pat) = Constrintern.interp_constrpattern Evd.empty (Global.env()) pat
   in
@@ -279,13 +279,13 @@ let match_dpat dp cls gls =
               (is_matching concld.d_typ cl) &
               (is_matching concld.d_sort (pf_type_of gls cl)))
             hl)
-        then error "No match"
+        then error "No match."
     | ({onhyps=Some[]},ConclLocation concld) when onconcl ->
         let cl = pf_concl gls in
         if not
           ((is_matching concld.d_typ cl) &
            (is_matching concld.d_sort (pf_type_of gls cl)))
-        then error "No match"
+        then error "No match."
     | _ -> error "ApplyDestructor"
 
 let forward_interp_tactic = 
@@ -304,8 +304,8 @@ let applyDestructor cls discard dd gls =
               ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in
             TacLetIn (false, [(dummy_loc, x), arg], tac)
         | None, (None, tac) -> tac
-        | _, (Some _,_) -> error "Destructor expects an hypothesis"
-        | _, (None,_) -> error "Destructor is for conclusion")
+        | _, (Some _,_) -> error "Destructor expects an hypothesis."
+        | _, (None,_) -> error "Destructor is for conclusion.")
       cll in
   let discard_0 =
     List.map (fun cl ->
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 70bc9a5924..eae6f56325 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -74,11 +74,11 @@ let prolog_tac l n gl =
   let n =
     match n with
       |  ArgArg n -> n
-      | _ -> error "Prolog called with a non closed argument"
+      | _ -> error "Prolog called with a non closed argument."
   in
   try (prolog l n gl)
   with UserError ("Refiner.tclFIRST",_) ->
-    errorlabstrm "Prolog.prolog" (str "Prolog failed")
+    errorlabstrm "Prolog.prolog" (str "Prolog failed.")
 
 TACTIC EXTEND prolog
 | [ "prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
@@ -331,7 +331,7 @@ let e_depth_search debug p db_list local_db gl =
     let tac = if debug then Search.debug_depth_first else Search.depth_first in
     let s = tac (make_initial_state p gl db_list local_db) in
     s.tacres
-  with Not_found -> error "EAuto: depth first search failed"
+  with Not_found -> error "eauto: depth first search failed."
 
 let e_breadth_search debug n db_list local_db gl =
   try
@@ -340,7 +340,7 @@ let e_breadth_search debug n db_list local_db gl =
     in
     let s = tac (make_initial_state n gl db_list local_db) in
     s.tacres
-  with Not_found -> error "EAuto: breadth first search failed"
+  with Not_found -> error "eauto: breadth first search failed."
 
 let e_search_auto debug (in_depth,p) lems db_list gl = 
   let local_db = make_local_hint_db true lems gl in 
@@ -359,7 +359,7 @@ let eauto debug np lems dbnames =
     List.map
       (fun x -> 
 	 try searchtable_map x
-	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
+	 with Not_found -> error ("No such Hint database: "^x^"."))
       ("core"::dbnames) 
   in
   tclTRY (e_search_auto debug np lems db_list)
@@ -377,12 +377,12 @@ let gen_eauto d np lems = function
 let make_depth = function
   | None -> !default_search_depth 
   | Some (ArgArg d) -> d
-  | _ -> error "EAuto called with a non closed argument"
+  | _ -> error "eauto called with a non closed argument."
 
 let make_dimension n = function
   | None -> (true,make_depth n)
   | Some (ArgArg d) -> (false,d)
-  | _ -> error "EAuto called with a non closed argument"
+  | _ -> error "eauto called with a non closed argument."
 
 open Genarg
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 43ea91f5ac..f0cc50d49e 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -115,7 +115,7 @@ let inductive_of = function
   | IndRef ity -> ity
   | r ->
       errorlabstrm "Decompose"
-        (Printer.pr_global r ++ str " is not an inductive type")
+        (Printer.pr_global r ++ str " is not an inductive type.")
 
 let decompose_these c l gls =
   let indl = (*List.map inductive_of*) l in 
@@ -182,7 +182,7 @@ let double_ind h1 h2 gls =
   let (abs_i,abs_j) =
     if abs_i < abs_j then (abs_i,abs_j) else
     if abs_i > abs_j then (abs_j,abs_i) else
-      error "Both hypotheses are the same" in
+      error "Both hypotheses are the same." in
   (tclTHEN (tclDO abs_i intro)
      (onLastHyp
        	(fun id ->
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 61100f0a50..625a096625 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -152,14 +152,14 @@ let decideGralEquality g =
     let rectype =
       match kind_of_term headtyp with
         | Ind mi -> mi
-	| _ -> error "This decision procedure only works for inductive objects"
+	| _ -> error"This decision procedure only works for inductive objects."
     in
     (tclTHEN
       (mkBranches c1 c2)
       (tclORELSE (h_solveNoteqBranch eqonleft) (solveEqBranch rectype)))
     g
   with PatternMatchingFailure ->
-    error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}"
+    error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}."
 
 let decideEqualityGoal = tclTHEN intros decideGralEquality
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 329284136d..8831a9e572 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -97,7 +97,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl =
     | None -> 
 	if l = NoBindings
 	then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl
-	else error "The term provided does not end with an equation" 
+	else error "The term provided does not end with an equation."
     | Some (hdcncl,_) -> 
 	if occs <> all_occurrences then (
 	  !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl)
@@ -109,7 +109,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl =
 	  let elim =
 	    try pf_global gl (id_of_string rwr_thm)
 	    with Not_found ->
-	      error ("Cannot find rewrite principle "^rwr_thm)
+	      error ("Cannot find rewrite principle "^rwr_thm^".")
 	  in 
 	    try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
 	    with e -> 
@@ -258,7 +258,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl =
 	 ]
       ] gl
   else
-    error "terms do not have convertible types"
+    error "Terms do not have convertible types."
   
 
 let replace c2 c1 gl = multi_replace onConcl c2 c1 false None gl
@@ -483,7 +483,7 @@ let construct_discriminator sigma env dirn c sort =
        *)
       errorlabstrm "Equality.construct_discriminator"
 	(str "Cannot discriminate on inductive constructors with 
-		 dependent types") in
+		 dependent types.") in
   let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
   let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in
@@ -523,7 +523,7 @@ let gen_absurdity id gl =
     simplest_elim (mkVar id) gl
   else
     errorlabstrm "Equality.gen_absurdity" 
-      (str "Not the negation of an equality")
+      (str "Not the negation of an equality.")
 
 (* Precondition: eq is leibniz equality
  
@@ -548,7 +548,7 @@ let apply_on_clause (f,t) clause =
   let argmv = 
     (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
-     | _  -> errorlabstrm "" (str "Ill-formed clause applicator")) in
+     | _  -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
   clenv_fchain argmv f_clause clause
 
 let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
@@ -569,7 +569,7 @@ let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
   let env = pf_env gls in
   match find_positions env sigma t1 t2 with
     | Inr _ ->
-	errorlabstrm "discr" (str"Not a discriminable equality")
+	errorlabstrm "discr" (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
 	let sort = pf_apply get_type_of gls (pf_concl gls) in 
 	discr_positions env sigma u eq_clause cpath dirn sort gls
@@ -583,7 +583,7 @@ let onEquality with_evars tac (c,lbindc) gls =
   let eq =
     try find_eq_data_decompose eqn
     with PatternMatchingFailure ->
-      errorlabstrm "" (str"No primitive equality found") in
+      errorlabstrm "" (str"No primitive equality found.") in
   tclTHEN
     (Refiner.tclEVARS (Evd.evars_of eq_clause'.evd)) 
     (tac eq eq_clause') gls
@@ -596,7 +596,7 @@ let onNegatedEquality with_evars tac gls =
         (onLastHyp (fun id -> 
           onEquality with_evars tac (mkVar id,NoBindings))) gls
   | _ -> 
-      errorlabstrm "" (str "Not a negated primitive equality")
+      errorlabstrm "" (str "Not a negated primitive equality.")
 
 let discrSimpleClause with_evars = function
   | None -> onNegatedEquality with_evars discrEq
@@ -613,7 +613,7 @@ let discrEverywhere with_evars =
       (Tacticals.tryAllHyps
         (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
     (fun gls -> 
-       errorlabstrm "DiscrEverywhere" (str"No discriminable equalities"))
+       errorlabstrm "DiscrEverywhere" (str"No discriminable equalities."))
 
 let discr_tac with_evars = function
   | None -> discrEverywhere with_evars
@@ -714,7 +714,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	(* the_conv_x had a side-effect on evdref *)
 	dflt
       else
-	error "Cannot solve an unification problem"
+	error "Cannot solve an unification problem."
     else
       let (a,p_i_minus_1) = match whd_beta_stack p_i with
 	| (_sigS,[a;p]) -> (a,p)
@@ -856,7 +856,7 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns =
 	(pf,ty))
       posns in
   if injectors = [] then
-    errorlabstrm "Equality.inj" (str "Failed to decompose the equality");
+    errorlabstrm "Equality.inj" (str "Failed to decompose the equality.");
   tclMAP
     (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
     injectors
@@ -870,10 +870,10 @@ let injEq ipats (eq,(t,t1,t2)) eq_clause =
   match find_positions env sigma t1 t2 with
     | Inl _ ->
 	errorlabstrm "Inj"
-	  (str"Not a projectable equality but a discriminable one")
+	  (str"Not a projectable equality but a discriminable one.")
     | Inr [] ->
 	errorlabstrm "Equality.inj" 
-	   (str"Nothing to do, it is an equality between convertible terms")
+	   (str"Nothing to do, it is an equality between convertible terms.")
     | Inr posns ->
 (* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ?
 	let t1 = try_delta_expand env sigma t1 in
@@ -977,7 +977,7 @@ let find_elim sort_of_gl lbeq =
         (match lbeq.rect with
            | Some eq_rect -> eq_rect
            | None -> errorlabstrm "find_elim"
-		 (str "this type of substitution is not allowed"))
+		 (str "This type of substitution is not allowed."))
 
 (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *)
 
@@ -1077,11 +1077,10 @@ let try_rewrite tac gls =
     tac gls
   with 
     | PatternMatchingFailure ->
-	errorlabstrm "try_rewrite" (str "Not a primitive equality here")
+	errorlabstrm "try_rewrite" (str "Not a primitive equality here.")
     | e when catchable_exception e -> 
 	errorlabstrm "try_rewrite"
-          (str "Cannot find a well-typed generalization of the goal that" ++
-             str " makes the proof progress")
+          (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
 
 let cutSubstClause l2r eqn cls gls =
   match cls with
@@ -1136,7 +1135,7 @@ let unfold_body x gl =
     match Sign.lookup_named x hyps with
         (_,Some xval,_) -> xval
       | _ -> errorlabstrm "unfold_body"
-          (pr_id x ++ str" is not a defined hypothesis") in
+          (pr_id x ++ str" is not a defined hypothesis.") in
   let aft = afterHyp x gl in
   let hl = List.fold_right 
     (fun (y,yval,_) cl -> ((all_occurrences_expr,y),InHyp) :: cl) aft [] in
@@ -1173,7 +1172,8 @@ let subst_one x gl =
       let test hyp _ = is_eq_x varx hyp in
       Sign.fold_named_context test ~init:() hyps;
       errorlabstrm "Subst"
-        (str "cannot find any non-recursive equality over " ++ pr_id x)
+        (str "Cannot find any non-recursive equality over " ++ pr_id x ++
+	 str".")
     with FoundHyp res -> res
   in
   (* The set of hypotheses using x *)
@@ -1254,7 +1254,7 @@ let cond_eq_term c t gl =
 
 let rewrite_multi_assumption_cond cond_eq_term cl gl = 
   let rec arec = function 
-    | [] -> error "No such assumption"
+    | [] -> error "No such assumption."
     | (id,_,t) ::rest -> 
 	begin 
 	  try 
@@ -1277,7 +1277,7 @@ let replace_multi_term dir_opt c  =
 (* JF. old version 
 let rewrite_assumption_cond faildir gl =
    let rec arec = function
-      | [] -> error "No such assumption"
+      | [] -> error "No such assumption."
       | (id,_,t)::rest ->
 	  (try let dir = faildir t gl in
 	       general_rewrite dir (mkVar id) gl
@@ -1287,7 +1287,7 @@ let rewrite_assumption_cond faildir gl =
 
 let rewrite_assumption_cond_in faildir hyp gl =
    let rec arec = function
-      | [] -> error "No such assumption"
+      | [] -> error "No such assumption."
       | (id,_,t)::rest ->
 	  (try let dir = faildir t gl in
 	       general_rewrite_in dir hyp (mkVar id) gl
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index bb279b5ba0..8313a09475 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -41,16 +41,16 @@ let instantiate n rawc ido gl =
 		  (match decl with 
 		      (_,None,typ) -> evar_list sigma typ
 		    | _ -> error 
-			"please be more specific : in type or value ?")
+			"Please be more specific: in type or value?")
 	      | InHypTypeOnly ->
 		  let (_, _, typ) = decl in evar_list sigma typ
 	      | InHypValueOnly ->
 		  (match decl with 
 		      (_,Some body,_) -> evar_list sigma body
-		    | _ -> error "not a let .. in  hypothesis") in
+		    | _ -> error "Not a defined hypothesis.") in
     if List.length evl < n then
       error "not enough uninstantiated existential variables";
-    if n <= 0 then error "incorrect existential variable index";
+    if n <= 0 then error "Incorrect existential variable index.";
     let ev,_ =  destEvar (List.nth evl (n-1)) in
     let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in
       tclTHEN
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 302d9a9926..4145a8dcc7 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -273,7 +273,7 @@ let dest_nf_eq gls eqn =
   try
     snd (first_match (match_eq_nf gls eqn) equalities)
   with PatternMatchingFailure ->
-    error "Not an equality"
+    error "Not an equality."
 
 (*** Sigma-types *)
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index a25fa285b1..6edc723cf2 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -101,7 +101,7 @@ let make_inv_predicate env sigma indf realargs id status concl =
       | Dep dflt_concl ->
 	  if not (occur_var env id concl) then
 	    errorlabstrm "make_inv_predicate"
-              (str "Current goal does not depend on " ++ pr_id id);
+              (str "Current goal does not depend on " ++ pr_id id ++ str".");
           (* We abstract the conclusion of goal with respect to
              realargs and c to * be concl in order to rewrite and have
              c also rewritten when the case * will be done *)
@@ -291,7 +291,7 @@ let generalizeRewriteIntros tac depids id gls =
 let rec tclMAP_i n tacfun = function
   | [] -> tclDO n (tacfun None)
   | a::l -> 
-      if n=0 then error "Too much names"
+      if n=0 then error "Too much names."
       else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
 
 let remember_first_eq id x = if !x = None then x := Some id
@@ -377,22 +377,22 @@ let rewrite_equations_gene othin neqns ba gl =
 
 let rec get_names allow_conj = function
   | IntroWildcard ->
-      error "Discarding pattern not allowed for inversion equations"
+      error "Discarding pattern not allowed for inversion equations."
   | IntroAnonymous ->
-      error "Anonymous pattern not allowed for inversion equations"
+      error "Anonymous pattern not allowed for inversion equations."
   | IntroFresh _->
-      error "Fresh pattern not allowed for inversion equations"
+      error "Fresh pattern not allowed for inversion equations."
   | IntroRewrite _->
-      error "Rewriting pattern not allowed for inversion equations"
+      error "Rewriting pattern not allowed for inversion equations."
   | IntroOrAndPattern [l] -> 
       if allow_conj then
 	if l = [] then (None,[]) else
 	  let l = List.map (fun id -> Option.get (fst (get_names false id))) l in
 	  (Some (List.hd l), l)
       else
-	error "Nested conjunctive patterns not allowed for inversion equations"
+	error"Nested conjunctive patterns not allowed for inversion equations."
   | IntroOrAndPattern l ->
-      error "Disjunctive patterns not allowed for inversion equations"
+      error "Disjunctive patterns not allowed for inversion equations."
   | IntroIdentifier id ->
       (Some id,[id])
 
@@ -453,7 +453,7 @@ let raw_inversion inv_kind id status names gl =
     try pf_reduce_to_atomic_ind gl (pf_type_of gl c)
     with UserError _ -> 
       errorlabstrm "raw_inversion"
-	(str ("The type of "^(string_of_id id)^" is not inductive")) in
+	(str ("The type of "^(string_of_id id)^" is not inductive.")) in
   let indclause = mk_clenv_from gl (c,t) in
   let ccl = clenv_type indclause in
   check_no_metas indclause ccl;
@@ -494,7 +494,7 @@ let not_found_message ids =
 let dep_prop_prop_message id =
   errorlabstrm "Inv"
     (str "Inversion on " ++ pr_id id ++
-       str " would needs dependent elimination Prop-Prop")
+       str " would need dependent elimination from Prop to Prop.")
  
 let not_inductive_here id =
   errorlabstrm "mind_specif_of_mind"
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index b43466e312..c1f20e8c35 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -214,7 +214,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
        (ids_of_named_context (named_context invEnv)));
   (*
     errorlabstrm "lemma_inversion"
-    (str"Computed inversion goal was not closed in initial signature");
+    (str"Computed inversion goal was not closed in initial signature.");
   *)
   let invSign = named_context_val invEnv in
   let pfs = mk_pftreestate (mk_goal invSign invGoal None) in
@@ -272,7 +272,7 @@ let inversion_lemma_from_goal n na (loc,id) sort dep_option inv_op =
     errorlabstrm "lemma_inversion"
       (str"Cannot compute lemma inversion when there are" ++ spc () ++
 	 str"free variables in the types of an inductive" ++ spc () ++
-	 str"which are not free in its instance"); *)
+	 str"which are not free in its instance."); *)
   add_inversion_lemma na env sigma t sort dep_option inv_op
    
 let add_inversion_lemma_exn na com comsort bool tac =
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 3dc8294627..39567f9810 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -229,7 +229,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with
   (* Produit. Est-ce bien exact ? *)
   | Prod (_,_,_) ->
       if occur_meta c then
-	error "Refine: proof term contains metas in a product"
+	error "refine: proof term contains metas in a product."
       else
       	TH (c,[],[])
 
@@ -330,7 +330,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
     | Fix ((ni,_),(fi,ai,_)) , _ ->
 	let out_name = function
 	  | Name id -> id
-          | _ -> error "recursive functions must have names !"
+          | _ -> error "Recursive functions must have names."
 	in
 	let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
 	tclTHENS
@@ -345,7 +345,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
     | CoFix (_,(fi,ai,_)) , _ ->
 	let out_name = function
 	  | Name id -> id
-          | _ -> error "recursive functions must have names !"
+          | _ -> error "Recursive functions must have names."
 	in
 	let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
 	tclTHENS
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index fc3673e6f4..f81f15d891 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -57,7 +57,7 @@ let safe_msgnl s =
 let error_syntactic_metavariables_not_allowed loc =
   user_err_loc 
     (loc,"out_ident",
-     str "Syntactic metavariables allowed only in quotations")
+     str "Syntactic metavariables allowed only in quotations.")
 
 let error_global_not_found_loc (loc,qid) = error_global_not_found_loc loc qid
 
@@ -111,7 +111,7 @@ type interp_sign =
 
 let check_is_value = function
   | VRTactic _ -> (* These are goals produced by Match *)
-   error "Immediate match producing tactics not allowed in local definitions"
+   error "Immediate match producing tactics not allowed in local definitions."
   | _ -> ()
 
 (* For tactic_of_value *)
@@ -121,7 +121,7 @@ exception NotTactic
 let constr_of_VConstr_context = function
   | VConstr_context c -> c
   | _ ->
-    errorlabstrm "constr_of_VConstr_context" (str "not a context variable")
+    errorlabstrm "constr_of_VConstr_context" (str "Not a context variable.")
 
 (* Displays a value *)
 let rec pr_value env = function
@@ -192,7 +192,7 @@ let find_reference env qid =
 let error_not_evaluable s =
   errorlabstrm "evalref_of_ref" 
     (str "Cannot coerce" ++ spc ()  ++ s ++ spc () ++
-     str "to an evaluable reference")
+     str "to an evaluable reference.")
 
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 let atomic_mactab = ref Idmap.empty
@@ -260,7 +260,7 @@ let tac_tab = Hashtbl.create 17
 let add_tactic s t =
   if Hashtbl.mem tac_tab s then
     errorlabstrm ("Refiner.add_tactic: ") 
-      (str ("Cannot redeclare tactic "^s));
+      (str ("Cannot redeclare tactic "^s^"."));
   Hashtbl.add tac_tab s t
 
 let overwriting_add_tactic s t =
@@ -275,7 +275,7 @@ let lookup_tactic s =
     Hashtbl.find tac_tab s
   with Not_found -> 
     errorlabstrm "Refiner.lookup_tactic"
-      (str"The tactic " ++ str s ++ str" is not installed")
+      (str"The tactic " ++ str s ++ str" is not installed.")
 (*
 let vernac_tactic (s,args) =
   let tacfun = lookup_tactic s args in
@@ -312,7 +312,7 @@ let lookup_genarg_subst  id = let (_,_,f) = lookup_genarg id in f
 let coerce_to_tactic loc id = function
   | VTactic _ | VFun _ | VRTactic _ as a -> a
   | _ -> user_err_loc 
-  (loc, "", str "variable " ++  pr_id id ++ str " should be bound to a tactic")
+  (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
 
 (*****************)
 (* Globalization *)
@@ -641,7 +641,7 @@ let extern_tacarg ch env sigma = function
   | VConstr c -> !print_xml_term ch env sigma c
   | VTactic _ | VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _
   | VIntroPattern _  | VRec _ | VList _ ->
-      error "Only externing of terms is implemented"
+      error "Only externing of terms is implemented."
 
 let extern_request ch req gl la =
   output_string ch "<REQUEST req=\""; output_string ch req;
@@ -679,7 +679,7 @@ let extract_let_names lrc =
     (fun ((loc,name),_) l ->
       if List.mem name l then
 	user_err_loc
-	  (loc, "glob_tactic", str "This variable is bound several times");
+	  (loc, "glob_tactic", str "This variable is bound several times.");
       name::l)
     lrc []
 
@@ -1019,8 +1019,8 @@ let read_pattern lfun = function
 let cons_and_check_name id l =
   if List.mem id l then
     user_err_loc (dloc,"read_match_context_hyps",
-      str ("Hypothesis pattern-matching variable "^(string_of_id id)^
-      " used twice in the same pattern"))
+      strbrk ("Hypothesis pattern-matching variable "^(string_of_id id)^
+      " used twice in the same pattern."))
   else id::l
 
 let rec read_match_context_hyps lfun lidh = function
@@ -1160,8 +1160,8 @@ let debugging_exception_step ist signal_anomaly e pp =
 
 let error_ltac_variable loc id env v s =
    user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ 
-   str " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ 
-   strbrk "which cannot be coerced to " ++ str s)
+   strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ 
+   strbrk "which cannot be coerced to " ++ str s ++ str".")
 
 exception CannotCoerceTo of string
 
@@ -1221,8 +1221,9 @@ let coerce_to_int = function
 
 let interp_int ist locid =
   try try_interp_ltac_var coerce_to_int ist None locid
-  with Not_found -> user_err_loc(fst locid,"interp_int",
-				str "Unbound variable"  ++ pr_id (snd locid))
+  with Not_found ->
+    user_err_loc(fst locid,"interp_int",
+      str "Unbound variable"  ++ pr_id (snd locid) ++ str".")
 
 let interp_int_or_var ist = function
   | ArgVar locid -> interp_int ist locid
@@ -1259,7 +1260,7 @@ let interp_hyp ist gl (loc,id as locid) =
   with Not_found -> 
   (* Then look if bound in the proof context at calling time *)
   if is_variable env id then id
-  else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found")
+  else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found.")
 
 let hyp_list_of_VList env = function
   | VList l -> List.map (coerce_to_hyp env) l
@@ -1277,7 +1278,7 @@ let interp_clause_pattern ist gl (l,occl) =
     | (hyp,l) :: rest ->
 	let hyp = interp_hyp ist gl hyp in
 	if List.mem hyp acc then
-	  error ("Hypothesis "^(string_of_id hyp)^" occurs twice");
+	  error ("Hypothesis "^(string_of_id hyp)^" occurs twice.");
 	(hyp,l)::(check (hyp::acc) rest)
     | [] -> []
   in (l,check [] occl)
@@ -1582,7 +1583,7 @@ let interp_may_eval f ist gl = function
       with
 	| Not_found ->
 	    user_err_loc (loc, "interp_may_eval",
-	    str "Unbound context identifier" ++ pr_id s))
+	    str "Unbound context identifier" ++ pr_id s ++ str"."))
   | ConstrTypeOf c -> pf_type_of gl (f ist gl c)
   | ConstrTerm c -> 
      try 
@@ -1627,7 +1628,7 @@ let rec interp_message ist = function
   | MsgIdent (loc,id) :: l ->
       let v =
 	try List.assoc id ist.lfun
-	with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found") in
+	with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found.") in
       pr_arg message_of_value v ++ interp_message ist l
 
 let rec interp_message_nl ist = function
@@ -1832,14 +1833,14 @@ and interp_app ist gl fv largs loc =
         VFun(newlfun@olfun,lvar,body)
     | _ ->
 	user_err_loc (loc, "Tacinterp.interp_app",
-          (str"Illegal tactic application"))
+          (str"Illegal tactic application."))
 
 (* Gives the tactic corresponding to the tactic value *)
 and tactic_of_value vle g =
   match vle with
   | VRTactic res -> res
   | VTactic (loc,tac) -> catch_error loc tac g
-  | VFun _ -> error "A fully applied tactic is expected"
+  | VFun _ -> error "A fully applied tactic is expected."
   | _ -> raise NotTactic
 
 (* Evaluation with FailError catching *)
@@ -1919,7 +1920,7 @@ and interp_match_context ist goal lz lr lmr =
               (v 0 (str "No matching clauses for match goal" ++
 		      (if ist.debug=DebugOff then
 			 fnl() ++ str "(use \"Set Ltac Debug\" for more info)"
-		       else mt())))
+		       else mt()) ++ str"."))
     end in
     apply_match_context ist env goal 0 lmr
       (read_match_rule (fst (constr_list ist env)) lmr)
@@ -2081,7 +2082,7 @@ and interp_match ist g lz constr lmr =
          with PatternMatchingFailure -> apply_match ist csr tl)
     | _ ->
       errorlabstrm "Tacinterp.apply_match" (str
-        "No matching clauses for match") in
+        "No matching clauses for match.") in
   let csr = 
       try interp_ltac_constr ist g constr with e ->
         debugging_exception_step ist true e
@@ -2139,13 +2140,13 @@ and interp_ltac_constr ist gl e =
             | VIntroPattern _ -> str "VIntroPattern"
             | VConstr_context _ -> str "VConstrr_context"
             | VRec _ -> str "VRec"
-            | VList _ -> str "VList"))
+            | VList _ -> str "VList") ++ str".")
 
 (* Interprets tactic expressions : returns a "tactic" *)
 and interp_tactic ist tac gl =
   try tactic_of_value (val_interp ist gl tac) gl
   with NotTactic ->
-    errorlabstrm "" (str "Must be a command or must give a tactic value")
+    errorlabstrm "" (str "Must be a command or must give a tactic value.")
 
 (* Interprets a primitive tactic *)
 and interp_atomic ist gl = function
@@ -2359,14 +2360,14 @@ and interp_atomic ist gl = function
     | ExtraArgType _ | BindingsArgType 
     | OptArgType _ | PairArgType _ 
     | List0ArgType _ | List1ArgType _ 
-	-> error "This generic type is not supported in alias"
+	-> error "This generic type is not supported in alias."
         
     in
     let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in
     let v = locate_tactic_call loc (val_interp { ist with lfun=lfun } gl body)
     in 
     try tactic_of_value v gl 
-    with NotTactic -> user_err_loc (loc,"",str "not a tactic")
+    with NotTactic -> user_err_loc (loc,"",str "Not a tactic.")
 
 let make_empty_glob_sign () =
   { ltacvars = ([],[]); ltacrecvars = []; 
@@ -2773,7 +2774,7 @@ let print_ltac id =
  with
   Not_found ->
    errorlabstrm "print_ltac"
-    (pr_qualid id ++ spc() ++ str "is not a user defined tactic")
+    (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
 
 open Libnames
 
@@ -2790,14 +2791,14 @@ let make_absolute_name ident repl =
 	if repl then id, kn
 	else
 	  user_err_loc (loc,"Tacinterp.add_tacdef",
-		       str "There is already an Ltac named " ++ pr_reference ident)
+		       str "There is already an Ltac named " ++ pr_reference ident ++ str".")
       else if is_atomic_kn kn then 
 	user_err_loc (loc,"Tacinterp.add_tacdef",
-		     str "Reserved Ltac name " ++ pr_reference ident)
+		     str "Reserved Ltac name " ++ pr_reference ident ++ str".")
       else id, kn
   with Not_found ->
     user_err_loc (loc,"Tacinterp.add_tacdef",
-		 str "There is no Ltac named " ++ pr_reference ident)
+		 str "There is no Ltac named " ++ pr_reference ident ++ str".")
 
 let rec filter_map f l = 
   let rec aux acc = function
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 3d5fd753ec..13ce334447 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -86,7 +86,7 @@ let tclMAP tacfun l =
 
 let tclNTH_HYP m (tac : constr->tactic) gl =
   tac (try mkVar(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id) 
-       with Failure _ -> error "No such assumption") gl
+       with Failure _ -> error "No such assumption.") gl
 
 (* apply a tactic to the last element of the signature  *)
 
@@ -94,11 +94,11 @@ let tclLAST_HYP = tclNTH_HYP 1
 
 let tclLAST_NHYPS n tac gl =
   tac (try list_firstn n (pf_ids_of_hyps gl)
-       with Failure _ -> error "No such assumptions") gl
+       with Failure _ -> error "No such assumptions.") gl
 
 let tclTRY_sign (tac : constr->tactic) sign gl =
   let rec arec = function
-    | []      -> tclFAIL 0 (str "no applicable hypothesis")
+    | []      -> tclFAIL 0 (str "No applicable hypothesis.")
     | [s]     -> tac (mkVar s) (*added in order to get useful error messages *)
     | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) 
   in 
@@ -218,7 +218,7 @@ let lastHyp gl = List.hd (pf_ids_of_hyps gl)
 
 let nLastHyps n gl =
   try list_firstn n (pf_hyps gl)
-  with Failure "firstn" -> error "Not enough hypotheses in the goal"
+  with Failure "firstn" -> error "Not enough hypotheses in the goal."
 
 
 let onClause t cls gl  = t cls gl
@@ -282,7 +282,7 @@ let compute_induction_names n = function
   | IntroOrAndPattern names when List.length names = n ->
       Array.of_list names
   | _ ->
-      errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names")
+      errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names.")
 
 let compute_construtor_signatures isrec (_,k as ity) =
   let rec analrec c recargs =
@@ -335,7 +335,7 @@ let general_elim_then_using mk_elim
   let indmv = 
     match kind_of_term (last_arg elimclause.templval.Evd.rebus) with
       | Meta mv -> mv
-      | _         -> error "elimination"
+      | _         -> anomaly "elimination"
   in
   let pmv =
     let p, _ = decompose_app elimclause.templtyp.Evd.rebus in
@@ -348,7 +348,7 @@ let general_elim_then_using mk_elim
 	      | Var id -> string_of_id id
 	      | _ -> "\b"
 	  in
-	  error ("The elimination combinator " ^ name_elim ^ " is not known") 
+	  error ("The elimination combinator " ^ name_elim ^ " is unknown.") 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause' in
   let elimclause' = clenv_match_args elimbindings elimclause' in
@@ -423,7 +423,7 @@ let make_elim_branch_assumptions ba gl =
 		   id::constargs,
 		   recargs,
 		   indargs) tl idtl
-      | (_, _) -> error "make_elim_branch_assumptions"
+      | (_, _) -> anomaly "make_elim_branch_assumptions"
   in 
   makerec ([],[],[],[],[]) ba.branchsign
     (try list_firstn ba.nassums (pf_hyps gl)
@@ -447,7 +447,7 @@ let make_case_branch_assumptions ba gl =
 		   id::cargs,
 		   recargs,
 		   id::constargs) tl idtl
-      | (_, _) -> error "make_case_branch_assumptions"
+      | (_, _) -> anomaly "make_case_branch_assumptions"
   in 
   makerec ([],[],[],[]) ba.branchsign
     (try list_firstn ba.nassums (pf_hyps gl)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c8f92b60f9..1fdd4c16fe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -98,7 +98,7 @@ let string_of_inductive c =
       let (mib,mip) = Global.lookup_inductive ind_sp in 
       string_of_id mip.mind_typename
   | _ -> raise Bound
-  with Bound -> error "Bound head variable"
+  with Bound -> error "Bound head variable."
 
 let rec head_constr_bound t l =
   let t = strip_outer_cast(collapse_appl t) in
@@ -114,7 +114,7 @@ let rec head_constr_bound t l =
     | _                -> raise Bound
 
 let head_constr c = 
-  try head_constr_bound c [] with Bound -> error "Bound head variable"
+  try head_constr_bound c [] with Bound -> error "Bound head variable."
 
 (*
 let bad_tactic_args s l =
@@ -174,7 +174,7 @@ let reduct_in_hyp redfun ((_,id),where) gl =
   match c with
   | None -> 
       if where = InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value");
+	errorlabstrm "" (pr_id id ++ str "has no value.");
       convert_hyp_no_check (id,None,redfun' ty) gl
   | Some b ->
       let b' = if where <> InHypTypeOnly then redfun' b else b in
@@ -197,7 +197,7 @@ let change_and_check cv_pb t env sigma c =
   if is_fconv cv_pb env sigma t c then 
     t
   else 
-    errorlabstrm "convert-check-hyp" (str "Not convertible")
+    errorlabstrm "convert-check-hyp" (str "Not convertible.")
 
 (* Use cumulutavity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb t = function
@@ -219,7 +219,7 @@ let change occl c cls =
       ({onhyps=(Some(_::_::_)|None)}
       |{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}),
       Some _ ->
-	error "No occurrences expected when changing several hypotheses"
+	error "No occurrences expected when changing several hypotheses."
     | _ -> ());
   onClauses (change_option occl c) cls
 
@@ -300,7 +300,7 @@ let find_name decl gl = function
   | IntroBasedOn (id,idl) -> fresh_id idl id gl
   | IntroMustBe id        -> 
       let id' = fresh_id [] id gl in
-      if id' <> id then error ((string_of_id id)^" is already used");
+      if id' <> id then error ((string_of_id id)^" is already used.");
       id'
 
 (* Returns the names that would be created by intros, without doing
@@ -337,7 +337,7 @@ let rec intro_gen name_flag move_flag force_flag gl =
 	    (reduce (Red true) onConcl)
 	    (intro_gen name_flag move_flag force_flag) gl
 	with Redelimination ->
-	  errorlabstrm "Intro" (str "No product even after head-reduction")
+	  errorlabstrm "Intro" (str "No product even after head-reduction.")
 
 let intro_mustbe_force id = intro_gen (IntroMustBe id) None true
 let intro_using id = intro_gen (IntroBasedOn (id,[])) None false
@@ -415,7 +415,8 @@ let depth_of_quantified_hypothesis red h gl =
         errorlabstrm "lookup_quantified_hypothesis" 
           (str "No " ++ msg_quantified_hypothesis h ++
 	  strbrk " in current goal" ++
-	  if red then strbrk " even after head-reduction" else mt ())
+	  (if red then strbrk " even after head-reduction" else mt ()) ++
+	  str".")
 
 let intros_until_gen red h g =
   tclDO (depth_of_quantified_hypothesis red h g) intro g
@@ -515,7 +516,7 @@ let cut c gl =
             (internal_cut_rev id c)
             (tclTHEN (apply_type t [mkVar id]) (thin [id]))
             gl
-    | _  -> error "Not a proposition or a type"
+    | _  -> error "Not a proposition or a type."
 
 let cut_intro t = tclTHENFIRST (cut t) intro
 
@@ -543,7 +544,7 @@ let cut_in_parallel l =
 let error_uninstantiated_metas t clenv =
   let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
   let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
-  in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id)
+  in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
 
 let clenv_refine_in with_evars id clenv gl =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
@@ -577,7 +578,7 @@ let elimination_clause_scheme with_evars allow_K elimclause indclause gl =
     (match kind_of_term (last_arg elimclause.templval.rebus) with
        | Meta mv -> mv
        | _  -> errorlabstrm "elimination_clause"
-             (str "The type of elimination clause is not well-formed")) 
+             (str "The type of elimination clause is not well-formed.")) 
   in
   let elimclause' = clenv_fchain indmv elimclause indclause in 
   res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags
@@ -648,7 +649,7 @@ let elimination_in_clause_scheme with_evars id elimclause indclause gl =
     match clenv_independent elimclause with
         [k1;k2] -> (k1,k2)
       | _  -> errorlabstrm "elimination_clause"
-          (str "The type of elimination clause is not well-formed") in
+          (str "The type of elimination clause is not well-formed.") in
   let elimclause'  = clenv_fchain indmv elimclause indclause in 
   let hyp = mkVar id in
   let hyp_typ = pf_type_of gl hyp in
@@ -658,7 +659,7 @@ let elimination_in_clause_scheme with_evars id elimclause indclause gl =
   let new_hyp_typ  = clenv_type elimclause'' in
   if eq_constr hyp_typ new_hyp_typ then
     errorlabstrm "general_rewrite_in" 
-      (str "Nothing to rewrite in " ++ pr_id id);
+      (str "Nothing to rewrite in " ++ pr_id id ++ str".");
   clenv_refine_in with_evars id elimclause'' gl
 
 let general_elim_in with_evars id =
@@ -701,7 +702,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl =
   let thm_ty0 = nf_betaiota (pf_type_of gl c) in
   let try_apply thm_ty nprod =
     let n = nb_prod thm_ty - nprod in
-    if n<0 then error "Apply: theorem has not enough premisses.";
+    if n<0 then error "Applied theorem has not enough premisses.";
     let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
     Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in
   try try_apply thm_ty0 concl_nprod
@@ -788,10 +789,10 @@ let find_matching_clause unifier clause =
 
 let progress_with_clause innerclause clause =
   let ordered_metas = List.rev (clenv_independent clause) in
-  if ordered_metas = [] then error "Statement without assumptions";
+  if ordered_metas = [] then error "Statement without assumptions.";
   let f mv = find_matching_clause (clenv_fchain mv clause) innerclause in
   try list_try_find f ordered_metas
-  with Failure _ -> error "Unable to unify"
+  with Failure _ -> error "Unable to unify."
 
 let apply_in_once gl innerclause (d,lbind) =
   let thm = nf_betaiota (pf_type_of gl d) in
@@ -832,7 +833,7 @@ let cut_and_apply c gl =
 	  tclTHENLAST
 	    (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
 	    (apply_term c [mkMeta (new_meta())]) gl
-      | _ -> error "Imp_elim needs a non-dependent product"
+      | _ -> error "lapply needs a non-dependent product."
 
 (********************************************************************)
 (*               Exact tactics                                      *)
@@ -844,7 +845,7 @@ let exact_check c gl =
   if pf_conv_x_leq gl ct concl then  
     refine_no_check c gl 
   else 
-    error "Not an exact proof"
+    error "Not an exact proof."
 
 let exact_no_check = refine_no_check
 
@@ -863,7 +864,7 @@ let (assumption : tactic) = fun gl ->
   let hyps = pf_hyps gl in
   let rec arec only_eq = function
     | [] -> 
-        if only_eq then arec false hyps else error "No such assumption"
+        if only_eq then arec false hyps else error "No such assumption."
     | (id,c,t)::rest -> 
 	if (only_eq & eq_constr t concl) 
           or (not only_eq & pf_conv_x_leq gl t concl)
@@ -919,7 +920,8 @@ let specialize mopt (c,lbind) g =
       let term = applist(thd,tstack) in 
       if occur_meta term then
 	errorlabstrm "" (str "Cannot infer an instance for " ++
-          pr_name (meta_name clause.evd (List.hd (collect_metas term))));
+          pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++
+	  str ".");
       Some (evars_of clause.evd), term
   in
   tclTHEN 
@@ -955,14 +957,14 @@ let keep hyps gl =
 (************************)
 
 let check_number_of_constructors expctdnumopt i nconstr =
-  if i=0 then error "The constructors are numbered starting from 1";
+  if i=0 then error "The constructors are numbered starting from 1.";
   begin match expctdnumopt with 
     | Some n when n <> nconstr ->
 	error ("Not an inductive goal with "^
-	       string_of_int n^plural n " constructor")
+	       string_of_int n^plural n " constructor"^".")
     | _ -> ()
   end;
-  if i > nconstr then error "Not enough constructors"
+  if i > nconstr then error "Not enough constructors."
 
 let constructor_tac with_evars expctdnumopt i lbind gl =
   let cl = pf_concl gl in 
@@ -987,7 +989,7 @@ let any_constructor with_evars tacopt gl =
   let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in
   let nconstr =
     Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
-  if nconstr = 0 then error "The type has no constructors";
+  if nconstr = 0 then error "The type has no constructors.";
   tclFIRST
     (List.map
       (fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t) 
@@ -1033,11 +1035,11 @@ let intro_or_and_pattern ll l' tac =
       | [] when n = 0 or tail -> []
       | [] -> IntroAnonymous :: adjust_names_length tail (n-1) []
       | _ :: _ as l when n = 0 -> 
-	  if tail then l else error "Too many names in some branch"
+	  if tail then l else error "Too many names in some branch."
       | ip :: l -> ip :: adjust_names_length tail (n-1) l in
     let ll = fix_empty_case nv ll in
     if List.length ll <> Array.length nv then
-      error "Not the right number of patterns";
+      error "Not the right number of patterns.";
     tclTHENLASTn
       (tclTHEN case_last clear_last)
       (array_map2 (fun n l -> tac ((adjust_names_length (l'=[]) n l)@l'))
@@ -1140,7 +1142,7 @@ let assert_as first ipat c gl =
       let id,tac = prepare_intros s ipat gl in
       tclTHENS ((if first then internal_cut else internal_cut_rev) id c)
 	(if first then [tclIDTAC; tac] else [tac; tclIDTAC]) gl
-  | _  -> error "Not a proposition or a type"
+  | _  -> error "Not a proposition or a type."
 
 let assert_tac first na = assert_as first (ipat_of_name na)
 let true_cut = assert_tac true 
@@ -1349,7 +1351,7 @@ let letin_tac with_eq name c occs gl =
     let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
     if name = Anonymous then fresh_id [] x gl else
       if not (mem_named_context x (pf_hyps gl)) then x else
-	error ("The variable "^(string_of_id x)^" is already declared") in
+	error ("The variable "^(string_of_id x)^" is already declared.") in
   let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in 
   let t = pf_type_of gl c in
   let newcl,eq_tac = match with_eq with
@@ -1390,7 +1392,7 @@ let unfold_body x gl =
     match Sign.lookup_named x hyps with
         (_,Some xval,_) -> xval
       | _ -> errorlabstrm "unfold_body"
-          (pr_id x ++ str" is not a defined hypothesis") in
+          (pr_id x ++ str" is not a defined hypothesis.") in
   let aft = afterHyp x gl in
   let hl = List.fold_right (fun (y,yval,_) cl -> (([],y),InHyp) :: cl) aft [] in
   let xvar = mkVar x in
@@ -1764,7 +1766,7 @@ let empty_scheme =
    hypothesis on which the induction is made *)
 let induction_tac with_evars (varname,lbind) typ scheme gl =
   let elimc,lbindelimc = 
-    match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in
+    match scheme.elimc with | Some x -> x | None -> error "No definition of the principle." in
   let elimt = scheme.elimt in
   let indclause = make_clenv_binding gl (mkVar varname,typ) lbind  in
   let elimclause =
@@ -1825,7 +1827,7 @@ let chop_context n l =
 
 let error_ind_scheme s =
   let s = if s <> "" then s^" " else s in
-  error ("Cannot recognise "^s^"an induction schema")
+  error ("Cannot recognize "^s^"an induction scheme.")
 
 let mkEq t x y = 
   mkApp (build_coq_eq (), [| t; x; y |])
@@ -2033,13 +2035,13 @@ let decompose_paramspred_branch_args elimt =
 	  then cut_noccur elimt' ((nme,None,tpe)::acc2)
 	  else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl
       | App(_, _) | Rel _ -> acc2 , [] , elimt
-      | _ -> error "cannot recognise an induction schema" in
+      | _ -> error_ind_scheme "" in
   let rec cut_occur elimt acc1 : rel_context * rel_context * rel_context * types =
     match kind_of_term elimt with
       | Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c ((nme,None,tpe)::acc1)
       | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl
       | App(_, _) | Rel _ -> acc1,[],[],elimt
-      | _ -> error "cannot recognise an induction schema" in
+      | _ -> error_ind_scheme "" in
   let acc1, acc2 , acc3, ccl = cut_occur elimt [] in
   (* Particular treatment when dealing with a dependent empty type elim scheme:
      if there is no branch, then acc1 contains all hyps which is wrong (acc1
@@ -2053,8 +2055,7 @@ let decompose_paramspred_branch_args elimt =
     let hd_ccl_pred,_ = decompose_app ccl in
     match kind_of_term hd_ccl_pred with
       | Rel i  -> let acc3,acc1 = cut_list (i-1) hyps in acc1 , [] , acc3 , ccl
-      | _ -> error "cannot recognize an induction schema"
-
+      | _ -> error_ind_scheme ""
 
 
 let exchange_hd_app subst_hd t =
@@ -2131,7 +2132,7 @@ let compute_elim_sig ?elimc elimt =
     (* 3- Look at last arg: is it the indarg? *)
     ignore (
       match List.hd args_indargs with
-	| hiname,Some _,hi -> error "cannot recognize an induction schema"
+	| hiname,Some _,hi -> error_ind_scheme ""
 	| hiname,None,hi -> 
 	    let hi_ind, hi_args = decompose_app hi in
 	    let hi_is_ind = (* hi est d'un type globalisable *)
@@ -2156,11 +2157,11 @@ let compute_elim_sig ?elimc elimt =
   with Exit -> (* Ending by computing indrev: *)
     match !res.indarg with
       | None -> !res (* No indref *)
-      | Some ( _,Some _,_) -> error "Cannot recognise an induction scheme"
+      | Some ( _,Some _,_) -> error_ind_scheme ""
       | Some ( _,None,ind) -> 
 	  let indhd,indargs = decompose_app ind in
 	  try {!res with indref = Some (global_of_constr indhd) }
-	  with _ -> error "Cannot find the inductive type of the inductive schema";;
+	  with _ -> error "Cannot find the inductive type of the inductive scheme.";;
 
 (* Check that the elimination scheme has a form similar to the 
    elimination schemes built by Coq. Schemes may have the standard
@@ -2174,7 +2175,7 @@ let compute_elim_signature elimc elimt names_info =
   let f,l = decompose_app scheme.concl in
   (* Vérifier que les arguments de Qi sont bien les xi. *)
   match scheme.indarg with
-    | Some (_,Some _,_) -> error "strange letin, cannot recognize an induction schema"
+    | Some (_,Some _,_) -> error "Strange letin, cannot recognize an induction scheme."
     | None -> (* Non standard scheme *)
 	let npred = List.length scheme.predicates in 
 	let is_pred n c = 
@@ -2242,7 +2243,7 @@ let compute_elim_signature elimc elimt names_info =
 		  list_lastn scheme.nargs indargs 
 		  = extended_rel_list 0 scheme.args in
 		if not (ccl_arg_ok & ind_is_ok) then
-		  error "Cannot recognize the conclusion of an induction schema";
+		  error_ind_scheme "the conclusion of";
 		[] 
 	in
 	let indsign = Array.of_list (find_branches 0 (List.rev scheme.branches)) in
@@ -2285,7 +2286,7 @@ let recolle_clenv scheme lid elimclause gl =
 	match kind_of_term x with
 	  | Meta mv -> mv
 	  | _  -> errorlabstrm "elimination_clause"
-              (str "The type of elimination clause is not well-formed"))
+              (str "The type of the elimination clause is not well-formed."))
       arr in
   let nmv = Array.length lindmv in
   let lidparams,lidargs = cut_list (scheme.nparams) lid in
@@ -2324,7 +2325,7 @@ let recolle_clenv scheme lid elimclause gl =
 let induction_tac_felim with_evars indvars (* (elimc,lbindelimc) elimt *) scheme gl = 
   let elimt = scheme.elimt in
   let elimc,lbindelimc = 
-    match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in
+    match scheme.elimc with | Some x -> x | None -> error "No definition of the principle." in
   (* elimclause contains this: (elimc ?i ?j ?k...?l) *)
   let elimclause =
     make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
@@ -2348,7 +2349,7 @@ let induction_from_context_l isrec with_evars elim_info lid names gl =
     + (if scheme.indarg <> None then 1 else 0) in
   (* Number of given induction args must be exact. *)
   if List.length lid <> nargs_indarg_farg + scheme.nparams then 
-      error "not the right number of arguments given to induction scheme";  
+      error "Not the right number of arguments given to induction scheme.";
   let env = pf_env gl in
   (* hyp0 is used for re-introducing hyps at the right place afterward.
      We chose the first element of the list of variables on which to
@@ -2466,7 +2467,7 @@ let induction_without_atomization isrec with_evars elim names lid gl =
   in
   let nlid = List.length lid in
   if nlid <> awaited_nargs
-  then error "Not the right number of induction arguments"
+  then error "Not the right number of induction arguments."
   else induction_from_context_l isrec with_evars elim_info lid names gl
 
 let new_induct_gen isrec with_evars elim names (c,lbind) cls gl =
@@ -2532,18 +2533,18 @@ let induct_destruct_l isrec with_evars lc elim names cls =
   let _ = 
     if elim = None
     then 
-      error ("Induction scheme must be given when several induction hypothesis.\n"
-      ^ "Example: induction x1 x2 x3 using my_scheme.") in
+      errorlabstrm "" (strbrk "Induction scheme must be given when several induction hypothesis are given.\n" ++ 
+      str "Example: induction x1 x2 x3 using my_scheme.") in
   let newlc = 
     List.map
       (fun x -> 
 	match x with (* FIXME: should we deal with ElimOnIdent? *)
 	  | ElimOnConstr (x,NoBindings) -> x
-	  | _ -> error "don't know where to find some argument")
+	  | _ -> error "Don't know where to find some argument.")
       lc in
   if cls <> None then
     error
-      "'in' clause not supported when several induction hypothesis are given";
+      "'in' clause not supported when several induction hypothesis are given.";
   new_induct_gen_l isrec with_evars elim names newlc
 
 (* Induction either over a term, over a quantified premisse, or over
@@ -2858,7 +2859,7 @@ let abstract_subproof name tac gl =
   let na = next_global_ident_away false name (pf_ids_of_hyps gl) in
   let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
     if occur_existential concl then
-      error "\"abstract\" cannot handle existentials";
+      error "\"abstract\" cannot handle existentials.";
     let lemme =
       start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ());
       let _,(const,kind,_) =
@@ -2901,7 +2902,7 @@ let admit_as_an_axiom gl =
   let name = add_suffix (get_current_proof_name ()) "_admitted" in
   let na = next_global_ident_away false name (pf_ids_of_hyps gl) in
   let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in
-  if occur_existential concl then error "\"admit\" cannot handle existentials";
+  if occur_existential concl then error"\"admit\" cannot handle existentials.";
   let axiom =
     let cd = Entries.ParameterEntry (concl,false) in
     let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 0207f1fb93..4af760ed8c 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -165,7 +165,7 @@ let tauto g =
   try intuition_gen (interp <:tactic<fail>>) g
   with
     Refiner.FailError _ | UserError _ ->
-      errorlabstrm "tauto" [< str "tauto failed" >]
+      errorlabstrm "tauto" (str "tauto failed.")
 
 let default_intuition_tac = interp <:tactic< auto with * >>