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

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

1 files changed, 17 insertions, 13 deletions

diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index e3674fae0e..79db4a9c45 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -247,7 +247,8 @@ let add_equation env e =
 (* accès a une equation *)
 let get_equation env id =
   try Hashtbl.find env.equations id
-  with e -> Printf.printf "Omega Equation %d non trouvée\n" id; raise e
+  with Not_found as e ->
+    Printf.printf "Omega Equation %d non trouvée\n" id; raise e
 
 (* Affichage des termes réifiés *)
 let rec oprint ch = function
@@ -349,7 +350,8 @@ let rec reified_of_formula env = function
       app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |]
 
 let reified_of_formula env f =
-  begin try reified_of_formula env f with e -> oprint stderr f; raise e end
+  try reified_of_formula env f
+  with reraise -> oprint stderr f; raise reraise
 
 let rec reified_of_proposition env = function
     Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) ->
@@ -380,8 +382,8 @@ let rec reified_of_proposition env = function
   | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |]
 
 let reified_of_proposition env f =
-  begin try reified_of_proposition env f
-  with e -> pprint stderr f; raise e end
+  try reified_of_proposition env f
+  with reraise -> pprint stderr f; raise reraise
 
 (* \subsection{Omega vers COQ réifié} *)
 
@@ -397,11 +399,8 @@ let reified_of_omega env body constant =
   List.fold_right mk_coeff body coeff_constant
 
 let reified_of_omega env body c  =
-  begin try
-    reified_of_omega env body c
-  with e ->
-    display_eq display_omega_var (body,c); raise e
-  end
+  try reified_of_omega env body c
+  with reraise -> display_eq display_omega_var (body,c); raise reraise
 
 (* \section{Opérations sur les équations}
 Ces fonctions préparent les traces utilisées par la tactique réfléchie
@@ -930,8 +929,12 @@ let filter_compatible_systems required systems =
 	if List.mem x required then select l
 	else if List.mem (barre x) required then raise Exit
 	else x :: select l
-    | [] -> [] in
-  List.map_filter (function (sol, splits) -> try Some (sol, select splits) with Exit -> None) systems
+    | [] -> []
+  in
+  List.map_filter
+    (function (sol, splits) ->
+      try Some (sol, select splits) with Exit -> None)
+    systems
 
 let rec equas_of_solution_tree = function
     Tree(_,t1,t2) -> (equas_of_solution_tree t1)@@(equas_of_solution_tree t2)
@@ -1000,10 +1003,11 @@ let rec solve_with_constraints all_solutions path =
   let weighted = filter_compatible_systems path all_solutions in
   let (winner_sol,winner_deps) =
     try select_smaller weighted
-    with e ->
+    with reraise ->
       Printf.printf "%d - %d\n"
 	(List.length weighted) (List.length all_solutions);
-      List.iter display_depend path; raise e in
+      List.iter display_depend path; raise reraise
+  in
   build_tree winner_sol (List.rev path) winner_deps
 
 let find_path {o_hyp=id;o_path=p} env =