diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /toplevel/mltop.ml4 | |
parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'toplevel/mltop.ml4')
-rw-r--r-- | toplevel/mltop.ml4 | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 2059ca60..f08308d3 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -92,8 +92,9 @@ let dir_ml_load s = (try t.load_obj s with | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u - | _ -> errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ - str s ++ str" to Coq code.")) + | e when Errors.noncritical e -> + errorlabstrm "Mltop.load_object" + (str"Cannot link ml-object " ++ str s ++ str" to Coq code.")) (* TO DO: .cma loading without toplevel *) | WithoutTop -> IFDEF HasDynlink THEN @@ -142,7 +143,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Names.id_of_string d - with _ -> + with e when Errors.noncritical e -> if_warn msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); flush_all (); @@ -269,9 +270,9 @@ let if_verbose_load verb f name fname = try f name fname; msgnl (str (info^" done]")); - with e -> + with reraise -> msgnl (str (info^" failed]")); - raise e + raise reraise (** Load a module for the first time (i.e. dynlink it) or simulate its reload (i.e. doing nothing except maybe |