From 033fed4d6788be791bb1c980f3cddc10827d6318 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 13 Mar 2013 00:00:59 +0000
Subject: Restrict (try...with...) to avoid catching critical exn (part 15)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16292 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/micromega/persistent_cache.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/micromega/persistent_cache.ml')

diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index cb7a9280d4..39a1b82b0d 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -82,10 +82,10 @@ let finally f rst =
   try
     let res = f () in
       rst () ; res
-  with x ->
+  with reraise ->
     (try rst ()
-    with _  -> raise x
-    ); raise x
+    with any -> raise reraise
+    ); raise reraise
 
 
 let read_key_elem inch =
@@ -93,7 +93,7 @@ let read_key_elem inch =
     Some (Marshal.from_channel inch)
   with
     | End_of_file -> None
-    |    _        -> raise InvalidTableFormat
+    | e when Errors.noncritical e -> raise InvalidTableFormat
 
 (** In win32, it seems that we should unlock the exact zone
     that has been locked, and not the whole file *)
@@ -151,7 +151,7 @@ let open_in f =
 	    Table.iter 
 	      (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
 	    flush outch ; 
-	  with  _ -> () )
+	  with e when Errors.noncritical e -> () )
 	    ;
 	    unlock out ; 
 	    { outch = outch ;
-- 
cgit v1.2.3