diff options
| author | herbelin | 2008-07-17 08:35:58 +0000 |
|---|---|---|
| committer | herbelin | 2008-07-17 08:35:58 +0000 |
| commit | d46b26156b306b8cb8b8867ec48dc43fd0c0e3fa (patch) | |
| tree | 4c6755e4b4df20e904610d023426ecac0febad91 /tactics/decl_interp.ml | |
| parent | cc1eab7783dfcbc6ed088231109553ec51eccc3f (diff) | |
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
Diffstat (limited to 'tactics/decl_interp.ml')
| -rw-r--r-- | tactics/decl_interp.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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) -> |