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

1 files changed, 11 insertions, 11 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f8ea1d528f..fdbd6cabd2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -72,16 +72,16 @@ let do_observe_tac s tac g =
     let v = tac g in 
     ignore(Stack.pop debug_queue);
     v
-  with e -> 
-    begin 
+  with reraise ->
+    begin
       if not (Stack.is_empty debug_queue)
       then
-	begin 
-	  let e : exn = Cerrors.process_vernac_interp_error e in
-	  print_debug_queue true e
+	begin
+	  let reraise : exn = Cerrors.process_vernac_interp_error reraise in
+	  print_debug_queue true reraise
 	end
-      ; 
-      raise e
+      ;
+      raise reraise
     end
 
 let observe_tac_stream s tac g =
@@ -145,7 +145,7 @@ let is_trivial_eq t =
 	    eq_constr t1 t2 && eq_constr a1 a2
 	| _ -> false
     end
-  with _ -> false
+  with e when Errors.noncritical e -> false
   in
 (*   observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *)
   res
@@ -171,7 +171,7 @@ let is_incompatible_eq t =
 	    (eq_constr u1 u2 &&
 	       incompatible_constructor_terms t1 t2)
 	| _ -> false
-    with _ -> false
+    with e when Errors.noncritical e -> false
   in
   if res then   observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t);
   res
@@ -258,7 +258,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	  then
 	    (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0))
 	  else nochange "not an equality"
-      with _ -> nochange "not an equality"
+      with e when Errors.noncritical e -> nochange "not an equality"
     in
     if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs";
     let rec compute_substitution sub t1 t2 =
@@ -629,7 +629,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 let my_orelse tac1 tac2 g =
   try
     tac1 g
-  with e ->
+  with e when Errors.noncritical e ->
 (*     observe (str "using snd tac since : " ++ Errors.print e); *)
     tac2 g