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

3 files changed, 10 insertions, 10 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index c30b2099f9..366fb77a01 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -1004,11 +1004,11 @@ let declare_include_ interp_struct me_asts =
 let protect_summaries f =
   let fs = Summary.freeze_summaries () in
   try f fs
-  with e ->
+  with reraise ->
     (* Something wrong: undo the whole process *)
-    let e = Errors.push e in
+    let reraise = Errors.push reraise in
     let () = Summary.unfreeze_summaries fs in
-    raise e
+    raise reraise
 
 let declare_include interp_struct me_asts =
   protect_summaries
diff --git a/library/impargs.ml b/library/impargs.ml
index 217169a610..56dca8e3f3 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -75,10 +75,10 @@ let with_implicits flags f x =
     let rslt = f x in
     implicit_args := oflags;
     rslt
-  with e ->
-    let e = Errors.push e in
+  with reraise ->
+    let reraise = Errors.push reraise in
     let () = implicit_args := oflags in
-    raise e
+    raise reraise
 
 let set_maximality imps b =
   (* Force maximal insertion on ending implicits (compatibility) *)
diff --git a/library/library.ml b/library/library.ml
index 0243968b9c..a5f93c02c1 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. *)