Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

6 files changed, 24 insertions, 17 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 6aa47eff..b7ee3c1a 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -397,8 +397,10 @@ let mono_filename f =
 	in
 	let id =
 	  if lang () <> Haskell then default_id
-	  else try id_of_string (Filename.basename f)
-	  with _ -> error "Extraction: provided filename is not a valid identifier"
+	  else
+            try id_of_string (Filename.basename f)
+	    with e when Errors.noncritical e ->
+              error "Extraction: provided filename is not a valid identifier"
 	in
 	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
 
@@ -473,8 +475,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
     msg_with ft (d.preamble mo opened unsafe_needs);
     msg_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 *)
@@ -487,8 +489,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
 	 msg_with ft (d.sig_preamble mo opened unsafe_needs);
 	 msg_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);
@@ -527,7 +529,9 @@ let rec locate_ref = function
   | r::l ->
       let q = snd (qualid_of_reference r) in
       let mpo = try Some (Nametab.locate_module q) with Not_found -> None
-      and ro = try Some (Smartlocate.global_with_alias r) with _ -> None
+      and ro =
+        try Some (Smartlocate.global_with_alias r)
+        with e when Errors.noncritical e -> None
       in
       match mpo, ro with
 	| None, None -> Nametab.error_global_not_found q
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0a17453c..e5357336 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -149,7 +149,7 @@ let rec handle_exn r n fn_name = function
 	 (fun i ->
 	    assert ((0 < i) && (i <= n));
 	    MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i)))
-       with _ -> MLexn s)
+       with e when Errors.noncritical e -> MLexn s)
   | a -> ast_map (handle_exn r n fn_name) a
 
 (*S Management of type variable contexts. *)
@@ -683,7 +683,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 6c78b533..b6fc5ac8 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -81,7 +81,9 @@ let kn_sig =
 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 e when Errors.noncritical e -> (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/mlutil.ml b/plugins/extraction/mlutil.ml
index a38b303f..d0bf387a 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -879,7 +879,7 @@ let is_program_branch = function
     (try
        ignore (int_of_string (String.sub s n (String.length s - n)));
        String.sub s 0 n = br
-     with _ -> false)
+     with e when Errors.noncritical e -> false)
   | Tmp _ | Dummy -> false
 
 let expand_linear_let o id e =
@@ -1312,7 +1312,7 @@ let inline_test r t =
     let c = match r with ConstRef c -> c | _ -> assert false in
     let has_body =
       try constant_has_body (Global.lookup_constant c)
-      with _ -> false
+      with e when Errors.noncritical e -> false
     in
     has_body &&
       (let t1 = eta_red t in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 289b2a1d..4e8d8145 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -119,7 +119,8 @@ let rec 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 e when Errors.noncritical e ->
+                   (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
@@ -188,7 +189,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
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index e0a6e843..497ddf03 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -255,7 +255,7 @@ let safe_basename_of_global r =
 
 let string_of_global r =
  try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
- with _ -> string_of_id (safe_basename_of_global r)
+ with e when Errors.noncritical e -> string_of_id (safe_basename_of_global r)
 
 let safe_pr_global r = str (string_of_global r)
 
@@ -263,7 +263,7 @@ let safe_pr_global r = str (string_of_global r)
 
 let safe_pr_long_global r =
   try Printer.pr_global r
-  with _ -> match r with
+  with e when Errors.noncritical e -> match r with
     | ConstRef kn ->
 	let mp,_,l = repr_con kn in
 	str ((string_of_mp mp)^"."^(string_of_label l))
@@ -452,7 +452,7 @@ let my_bool_option name initval =
 
 (*s Extraction AccessOpaque *)
 
-let access_opaque = my_bool_option "AccessOpaque" false
+let access_opaque = my_bool_option "AccessOpaque" true
 
 (*s Extraction AutoInline *)