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

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

4 files changed, 10 insertions, 8 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 358fe2d01..a64cc3d70 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -489,8 +489,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
     pp_with ft (d.preamble mo comment opened unsafe_needs);
     pp_with ft (d.pp_struct struc);
     Option.iter close_out cout;
-  with e ->
-    Option.iter close_out cout; raise e
+  with reraise ->
+    Option.iter close_out cout; raise reraise
   end;
   if not dry then Option.iter info_file fn;
   (* Now, let's print the signature *)
@@ -503,8 +503,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
 	 pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
 	 pp_with ft (d.pp_sig (signature_of_structure struc));
 	 close_out cout;
-       with e ->
-	 close_out cout; raise e
+       with reraise ->
+	 close_out cout; raise reraise
        end;
        info_file si)
     (if dry then None else si);
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 3ec9038c6..903a647fc 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -682,7 +682,7 @@ and extract_cst_app env mle mlt kn args =
 	let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
 	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
-      with _ -> mla
+      with e when Errors.noncritical e -> mla
   in
   (* For strict languages, purely logical signatures with at least
      one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 3925a2a2f..59dd5596e 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -86,7 +86,9 @@ let pp_global k r =
 let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ -> assert false
-    | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
+    | Tvar i ->
+      (try pr_id (List.nth vl (pred i))
+       with Failure _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global Type r
     | Tglob (IndRef(kn,0),l)
 	when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" ->
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 6c3054e2c..f3d6bcb98 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -127,7 +127,7 @@ let pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ | Taxiom -> assert false
     | Tvar i -> (try pp_tvar (List.nth vl (pred i))
-		 with _ -> (str "'a" ++ int i))
+                 with Failure _ -> (str "'a" ++ int i))
     | Tglob (r,[a1;a2]) when is_infix r ->
 	pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
     | Tglob (r,[]) -> pp_global Type r
@@ -196,7 +196,7 @@ let rec pp_expr par env args =
 	   let args = List.skipn (projection_arity r) args in
 	   let record = List.hd args in
 	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
-	 with _ -> apply (pp_global Term r))
+	 with e when Errors.noncritical e -> apply (pp_global Term r))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
 	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args