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

1 files changed, 9 insertions, 9 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 3d5fd753e..13ce33444 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)