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

7 files changed, 37 insertions, 36 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
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 7f05c3b0e2..09637d273f 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -363,7 +363,7 @@ let generate_functional_principle
      Don't forget to close the goal if an error is raised !!!!
   *)
   save false new_princ_name entry g_kind hook
-  with e ->
+  with e when Errors.noncritical e ->
     begin
       begin
 	try
@@ -375,7 +375,7 @@ let generate_functional_principle
 	  then Pfedit.delete_current_proof ()
 	  else ()
 	  else ()
-	with _ -> ()
+	with e when Errors.noncritical e -> ()
       end;
       raise (Defining_principle e)
     end
@@ -516,7 +516,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	0
 	(prove_princ_for_struct false 0 (Array.of_list funs))
 	(fun _ _ _ -> ())
-  with e ->
+  with e when Errors.noncritical e ->
     begin
       begin
 	try
@@ -528,7 +528,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	  then Pfedit.delete_current_proof ()
 	  else ()
 	  else ()
-	with _ -> ()
+	with e when Errors.noncritical e -> ()
       end;
       raise (Defining_principle e)
     end
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index ef2276134b..1ccfe3c31d 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -209,14 +209,14 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
 		    try Functional_principles_types.build_scheme fas
 		    with Functional_principles_types.No_graph_found ->
 		      Errors.error ("Cannot generate induction principle(s)")
-    		      | e ->
+		      | e when Errors.noncritical e ->
 			  let names = List.map (fun (_,na,_) -> na) fas in
 			  warning_error names e
 
 		  end
 	      | _ -> assert false (* we can only have non empty  list *)
 	  end
-	  | e -> 
+	  | e when Errors.noncritical e ->
 	      let names = List.map (fun (_,na,_) -> na) fas in
 	      warning_error names e
       end
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 9ec935cfdc..fe48cbd882 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -912,7 +912,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  try
 		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
 		    let t' =
-		      try Pretyping.understand Evd.empty env t with _ -> raise Continue
+		      try Pretyping.understand Evd.empty env t
+                      with e when Errors.noncritical e -> raise Continue
 		    in
 		    let is_in_b = is_free_in id b in
 		    let _keep_eq =
@@ -1211,7 +1212,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool)
 	     l := param::!l
 	)
 	rels_params.(0)
-    with _ ->
+    with e when Errors.noncritical e ->
       ()
   in
   List.rev !l
@@ -1417,7 +1418,7 @@ let do_build_inductive
 	in
 	observe (msg);
 	raise e
-    | e ->
+    | reraise ->
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
 	let repacked_rel_inds =
@@ -1428,16 +1429,16 @@ let do_build_inductive
 	  str "while trying to define"++ spc () ++
 	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
 	    ++ fnl () ++
-	    Errors.print e
+	    Errors.print reraise
 	in
  	observe msg;
-	raise e
+	raise reraise
 
 
 
 let build_inductive funnames funsargs returned_types rtl =
   try
     do_build_inductive funnames funsargs returned_types rtl
-  with e -> raise (Building_graph e)
+  with e when Errors.noncritical e -> raise (Building_graph e)
 
 
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 0159a0aeeb..6b4fbeef46 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -531,8 +531,8 @@ let rec are_unifiable_aux  = function
 	     then raise NotUnifiable
 	     else
 	       let eqs' =
- 		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly (Pp.str "are_unifiable_aux")
+		 try (List.combine cpl1 cpl2) @ eqs
+		 with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux")
 	       in
 	       are_unifiable_aux eqs'
 
@@ -553,8 +553,8 @@ let rec eq_cases_pattern_aux  = function
 	     then raise NotUnifiable
 	     else
 	       let eqs' =
- 		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly (Pp.str "eq_cases_pattern_aux")
+		 try (List.combine cpl1 cpl2) @ eqs
+		 with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux")
 	       in
 	       eq_cases_pattern_aux eqs'
 	 | _ -> raise NotUnifiable
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d58a6f038f..f0f76860a3 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -164,8 +164,8 @@ let build_newrecursive
 	       sigma rec_sign rec_impls def
 	  )
           lnameargsardef
-	with e ->
-	States.unfreeze fs; raise e in
+	with reraise ->
+	States.unfreeze fs; raise reraise in
     States.unfreeze fs; def
   in
   recdef,rec_impls
@@ -249,12 +249,12 @@ let derive_inversion fix_names =
 	   (fun id -> destInd (Constrintern.global_reference (mk_rel_id id)))
 	   fix_names
 	)
-    with e ->
+    with e when Errors.noncritical e ->
       let e' = Cerrors.process_vernac_interp_error e in
       msg_warning
 	(str "Cannot build inversion information" ++
 	   if do_observe () then (fnl() ++ Errors.print e') else mt ())
-  with _ -> ()
+  with e when Errors.noncritical e -> ()
 
 let warning_error names e =
   let e = Cerrors.process_vernac_interp_error e in
@@ -351,7 +351,7 @@ let generate_principle  on_error
 	Array.iter (add_Function is_general) funs_kn;
 	()
       end
-  with e ->
+  with e when Errors.noncritical e ->
     on_error names e
 
 let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
@@ -414,7 +414,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	   functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
 	);
       derive_inversion [fname]
-    with e ->
+    with e when Errors.noncritical e ->
       (* No proof done *)
       ()
   in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index d6a017d08c..56660cd69f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -118,7 +118,7 @@ let def_of_const t =
       (try (match Declareops.body_of_constant (Global.lookup_constant sp) with
              | Some c -> Lazyconstr.force c
 	     | _ -> assert false)
-       with _ -> assert false)
+       with Not_found -> assert false)
     |_ -> assert false
 
 let coq_constant s =
@@ -204,13 +204,13 @@ let with_full_print f a =
     Dumpglob.continue ();
     res
   with
-    | e ->
+    | reraise ->
 	Impargs.make_implicit_args old_implicit_args;
 	Impargs.make_strict_implicit_args old_strict_implicit_args;
 	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
 	Flags.raw_print := old_rawprint;
 	Dumpglob.continue ();
-	raise e
+	raise reraise