diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-17 08:35:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-17 08:35:58 +0000 |
| commit | d46b26156b306b8cb8b8867ec48dc43fd0c0e3fa (patch) | |
| tree | 4c6755e4b4df20e904610d023426ecac0febad91 /kernel/safe_typing.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 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fbd4901d6..eef2d675c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -163,7 +163,7 @@ let safe_push_named (id,_,_ as d) env = let _ = try let _ = lookup_named id env in - error ("identifier "^string_of_id id^" already defined") + error ("Identifier "^string_of_id id^" already defined.") with Not_found -> () in Environ.push_named d env @@ -446,7 +446,7 @@ let end_module l restype senv = let senv = add_constraints (struct_expr_constraints struct_expr) senv in let msid,str = match (eval_struct senv.env struct_expr) with | SEBstruct(msid,str_l) -> msid,str_l - | _ -> error ("You cannot Include a higher-order Module or Module Type" ) + | _ -> error ("You cannot Include a higher-order Module or Module Type.") in let mp_sup = senv.modinfo.modpath in let str1 = subst_signature_msid msid mp_sup str in @@ -660,7 +660,7 @@ let check_engagement env c = | Some ImpredicativeSet, Some ImpredicativeSet -> () | _, None -> () | _, Some ImpredicativeSet -> - error "Needs option -impredicative-set" + error "Needs option -impredicative-set." let set_engagement c senv = {senv with @@ -739,9 +739,10 @@ let check_imports senv needed = try let actual_stamp = List.assoc id imports in if stamp <> actual_stamp then - error ("Inconsistent assumptions over module " ^(string_of_dirpath id)) + error + ("Inconsistent assumptions over module "^(string_of_dirpath id)^".") with Not_found -> - error ("Reference to unknown module " ^ (string_of_dirpath id)) + error ("Reference to unknown module "^(string_of_dirpath id)^".") in List.iter check needed |