Restrict (try...with...) to avoid catching critical exn (part 8)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 4 deletions

diff --git a/library/library.ml b/library/library.ml
index 0243968b9..a5f93c02c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -406,7 +406,7 @@ let fetch_opaque_table (f,pos,digest) =
     let table = (System.marshal_in f ch : LightenLibrary.table) in
     close_in ch;
     table
-  with _ ->
+  with e when Errors.noncritical e ->
     error
       ("The file "^f^" is inaccessible or has changed,\n" ^
        "cannot load some opaque constant bodies in it.\n")
@@ -667,12 +667,12 @@ let save_library_to dir f =
       | 0 -> ()
       | _ -> anomaly (Pp.str "Library compilation failure")
     end
-  with e ->
-    let e = Errors.push e in
+  with reraise ->
+    let reraise = Errors.push reraise in
     let () = msg_warning (str ("Removed file "^f')) in
     let () = close_out ch in
     let () = Sys.remove f' in
-    raise e
+    raise reraise
 
 (************************************************************************)
 (*s Display the memory use of a library. *)