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 /pretyping/clenv.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 'pretyping/clenv.ml')
| -rw-r--r-- | pretyping/clenv.ml | 17 |
1 files changed, 9 insertions, 8 deletions
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 *) |