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

4 files changed, 12 insertions, 17 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index a5e7d6c4d..f8ea1d528 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1224,7 +1224,10 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	let ctxt,pte_app =  (decompose_prod_assum (pf_concl gl)) in
 	let pte,pte_args = (decompose_app pte_app) in
 	try
-	  let pte = try destVar pte with _ -> anomaly (Pp.str "Property is not a variable")  in
+	  let pte =
+            try destVar pte
+            with DestKO -> anomaly (Pp.str "Property is not a variable")
+          in
 	  let fix_info = Id.Map.find  pte ptes_to_fix in
 	  let nb_args = fix_info.nb_realargs in
 	  tclTHENSEQ
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 131b4c0e2..d58a6f038 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -85,10 +85,7 @@ let functional_induction with_clean c princl pat =
     let princ' = Some (princ,bindings) in
     let princ_vars =
       List.fold_right
-	(fun a acc ->
-	  try Id.Set.add (destVar a) acc
-	  with _ -> acc
-	)
+	(fun a acc -> try Id.Set.add (destVar a) acc with DestKO -> acc)
 	args
 	Id.Set.empty
     in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 67f6fdd54..d6a017d08 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -49,11 +49,8 @@ let locate_constant ref =
 
 
 let locate_with_msg msg f x =
-  try
-    f x
-  with
-    | Not_found -> raise (Errors.UserError("", msg))
-    | e -> raise e
+  try f x
+  with Not_found -> raise (Errors.UserError("", msg))
 
 
 let filter_map filter f =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index bea019259..d1005a8cd 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1491,7 +1491,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     let stop = 
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
 	  false
-      with e ->
+      with e when Errors.noncritical e ->
 	begin
 	  if do_observe ()
 	  then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
@@ -1526,10 +1526,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       using_lemmas
       (List.length res_vars)
       hook 
-  with e ->
-    begin
-      (try ignore (Backtrack.backto previous_label) with _ -> ());
-      (*       anomaly (Pp.str "Cannot create termination Lemma") *)
-      raise e
-    end
+  with reraise ->
+    ignore (Backtrack.backto previous_label);
+    (*       anomaly (Pp.str "Cannot create termination Lemma") *)
+    raise reraise