Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

49 files changed, 244 insertions, 178 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index d0f81dad..1c021eee 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -404,7 +404,8 @@ let rec canonize_name c =
 let build_subst uf subst =
   Array.map (fun i ->
 	       try term uf i
-	       with _ -> anomaly "incomplete matching") subst
+	       with e when Errors.noncritical e ->
+                 anomaly "incomplete matching") subst
 
 let rec inst_pattern subst = function
     PVar i ->
@@ -730,9 +731,7 @@ let __eps__ = id_of_string "_eps_"
 let new_state_var typ state =
   let id = pf_get_new_id __eps__ state.gls in
   let {it=gl ; sigma=sigma} = state.gls in
-  let new_hyps =
-    Environ.push_named_context_val (id,None,typ) (Goal.V82.hyps sigma gl) in
-  let gls = Goal.V82.new_goal_with sigma gl new_hyps in
+  let gls = Goal.V82.new_goal_with sigma gl [id,None,typ] in
     state.gls<- gls;
     id
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 95ff4d34..764e36b0 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -129,7 +129,9 @@ let non_trivial = function
 
 let patterns_of_constr env sigma nrels term=
   let f,args=
-    try destApp (whd_delta env term) with _ -> raise Not_found in
+    try destApp (whd_delta env term)
+    with e when Errors.noncritical e -> raise Not_found
+  in
 	if eq_constr f (Lazy.force _eq) && (Array.length args)=3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 730051c1..da88d48d 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -75,9 +75,9 @@ let mode_of_pftreestate pts =
       Mode_proof
 	  
 let get_current_mode () =
-  try 
+  try
     mode_of_pftreestate (Pfedit.get_pftreestate ())
-  with _ -> Mode_none
+  with e when Errors.noncritical e -> Mode_none
 
 let check_not_proof_mode str =
  if get_current_mode () = Mode_proof then
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 72caeaed..ab161b35 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -381,7 +381,7 @@ let find_subsubgoal c ctyp skip submetas gls =
 		  se.se_meta submetas se.se_meta_list}
 	  else
 	      dfs (pred n)
-      with _ ->
+      with e when Errors.noncritical e ->
 	begin
 	  enstack_subsubgoals env se stack gls;
 	  dfs n
@@ -519,7 +519,10 @@ let decompose_eq id gls =
 
 let instr_rew _thus rew_side cut gls0 =
   let last_id =
-    try get_last (pf_env gls0) with _ -> error "No previous equality." in
+    try get_last (pf_env gls0)
+    with e when Errors.noncritical e ->
+      error "No previous equality."
+  in
   let typ,lhs,rhs = decompose_eq last_id gls0 in
   let items_tac gls =
     match cut.cut_by with
@@ -849,7 +852,7 @@ let build_per_info etype casee gls =
   let ind =
     try
       destInd hd
-    with _ ->
+    with e when Errors.noncritical e ->
       error "Case analysis must be done on an inductive object." in
   let mind,oind = Global.lookup_inductive ind in
   let nparams,index =
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 *)
 
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 9d3d8c99..29d41b81 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -85,7 +85,7 @@ let gen_ground_tac flag taco ids bases gl=
 	extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
       let result=ground_tac solver startseq gl in
 	qflag:=backup;result
-    with e ->qflag:=backup;raise e
+    with reraise ->qflag:=backup;raise reraise
 
 (* special for compatibility with Intuition
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 68f112d6..4b07c609 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -129,7 +129,7 @@ let mk_open_instance id gl m t=
 	| _-> anomaly "can't happen" in
   let ntt=try
     Pretyping.Default.understand evmap env (raux m rawt)
-  with _ ->
+  with e when Errors.noncritical e ->
     error "Untypable instance, maybe higher-order non-prenex quantification" in
     decompose_lam_n_assum m ntt
 
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
index 043c9e51..1574e21e 100644
--- a/plugins/fourier/fourier.ml
+++ b/plugins/fourier/fourier.ml
@@ -175,7 +175,7 @@ let unsolvable lie =
 			raise (Failure "contradiction found"))
           |_->assert false)
 			     lr)
-   with _ -> ());
+   with e when Errors.noncritical e -> ());
    !res
 ;;
 
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index cdd10d70..e0e4f7d6 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -40,7 +40,7 @@ type flin = {fhom: rational Constrhash.t;
 
 let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};;
 
-let flin_coef f x = try (Constrhash.find f.fhom x) with _-> r0;;
+let flin_coef f x = try (Constrhash.find f.fhom x) with Not_found -> r0;;
 
 let flin_add f x c =
     let cx = flin_coef f x in
@@ -141,10 +141,12 @@ let rec flin_of_constr c =
 	     (try (let a=(rational_of_constr args.(0)) in
                      try (let b = (rational_of_constr args.(1)) in
 			    (flin_add_cste (flin_zero()) (rmult a b)))
-		     with _-> (flin_add (flin_zero())
+		     with e when Errors.noncritical e ->
+                       (flin_add (flin_zero())
 				 args.(1)
 				 a))
-	      with _-> (flin_add (flin_zero())
+	      with e when Errors.noncritical e ->
+                (flin_add (flin_zero())
 			  args.(0)
 			  (rational_of_constr args.(1))))
 	 | "Rinv"->
@@ -154,7 +156,8 @@ let rec flin_of_constr c =
 	     (let b=(rational_of_constr args.(1)) in
 		try (let a = (rational_of_constr args.(0)) in
 		       (flin_add_cste (flin_zero()) (rdiv a b)))
-		with _-> (flin_add (flin_zero())
+		with e when Errors.noncritical e ->
+                  (flin_add (flin_zero())
 		            args.(0)
                             (rinv b)))
          |_->assert false)
@@ -164,7 +167,8 @@ let rec flin_of_constr c =
               |"R0" -> flin_zero ()
               |_-> assert false)
   |_-> assert false)
-  with _ -> flin_add (flin_zero())
+  with e when Errors.noncritical e ->
+    flin_add (flin_zero())
                      c
 	             r1
 ;;
@@ -494,13 +498,13 @@ let rec fourier gl=
 	    |_->assert false)
         |_->assert false
       in tac gl)
-     with _ ->
+     with e when Errors.noncritical e ->
     (* les hypothèses *)
     let hyps = List.map (fun (h,t)-> (mkVar h,t))
                         (list_of_sign (pf_hyps gl)) in
     let lineq =ref [] in
     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
-		        with _ -> ())
+		        with e when Errors.noncritical e -> ())
               hyps;
     (* lineq = les inéquations découlant des hypothèses *)
     if !lineq=[] then Util.error "No inequalities";
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 33d77568..48205019 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -33,9 +33,12 @@ let observennl strm =
 
 let do_observe_tac s tac g =
  try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
- with e ->
-   let e = Cerrors.process_vernac_interp_error e in
-   let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
+ with reraise ->
+   let e = Cerrors.process_vernac_interp_error reraise in
+   let goal =
+     try (Printer.pr_goal g)
+     with e when Errors.noncritical e -> assert false
+   in
    msgnl (str "observation "++ s++str " raised exception " ++
 	    Errors.print e ++ str " on goal " ++ goal );
    raise e;;
@@ -119,7 +122,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
@@ -145,7 +148,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
@@ -232,7 +235,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 =
@@ -608,7 +611,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
 
@@ -1212,7 +1215,11 @@ 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 "Property is not a variable"  in
+	  let pte =
+            try destVar pte
+            with e when Errors.noncritical e ->
+              anomaly "Property is not a variable"
+          in
 	  let fix_info = Idmap.find  pte ptes_to_fix in
 	  let nb_args = fix_info.nb_realargs in
 	  tclTHENSEQ
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 00e966fb..04fcc8d4 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -302,11 +302,8 @@ let defined () =
 	  "defined"
 	  ((try
 	      str "On goal : " ++ fnl () ++  pr_open_subgoals () ++ fnl ()
-	    with _ -> mt ()
+	    with e when Errors.noncritical e -> mt ()
 	   ) ++msg)
-    | e -> raise e
-
-
 
 let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
@@ -401,7 +398,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
@@ -413,7 +410,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
@@ -554,7 +551,7 @@ let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition
 	0
 	(prove_princ_for_struct false 0 (Array.of_list funs))
 	(fun _ _ _ -> ())
-  with e ->
+  with e when Errors.noncritical e ->
     begin
       begin
 	try
@@ -566,7 +563,7 @@ let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition
 	  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 85d79214..6b6e4838 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -208,14 +208,14 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
 		    try Functional_principles_types.build_scheme fas
 		    with Functional_principles_types.No_graph_found ->
 		      Util.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 43b08840..b9e0e62a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -948,7 +948,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.Default.understand Evd.empty env t with _ -> raise Continue
+		      try Pretyping.Default.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 =
@@ -1247,7 +1248,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
 	     l := param::!l
 	)
 	rels_params.(0)
-    with _ ->
+    with e when Errors.noncritical e ->
       ()
   in
   List.rev !l
@@ -1453,7 +1454,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 =
@@ -1464,16 +1465,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 cdd0eaf7..6cc932b1 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -534,7 +534,8 @@ let rec are_unifiable_aux  = function
 	     else
 	       let eqs' =
  		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly "are_unifiable_aux"
+		 with e when Errors.noncritical e ->
+                   anomaly "are_unifiable_aux"
 	       in
 	       are_unifiable_aux eqs'
 
@@ -556,7 +557,8 @@ let rec eq_cases_pattern_aux  = function
 	     else
 	       let eqs' =
  		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly "eq_cases_pattern_aux"
+		 with e when Errors.noncritical e ->
+                   anomaly "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 8caeca57..d2c065a0 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -82,7 +82,7 @@ let functional_induction with_clean c princl pat =
       List.fold_right
 	(fun a acc ->
 	  try Idset.add (destVar a) acc
-	  with _ -> acc
+	  with e when Errors.noncritical e -> acc
 	)
 	args
 	Idset.empty
@@ -166,8 +166,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
@@ -251,12 +251,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
@@ -346,7 +346,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) =
@@ -413,7 +413,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 dd475315..827191b1 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -55,7 +55,6 @@ let locate_with_msg msg f x =
     f x
   with
     | Not_found -> raise (Util.UserError("", msg))
-    | e -> raise e
 
 
 let filter_map filter f =
@@ -123,7 +122,7 @@ let def_of_const t =
       (try (match Declarations.body_of_constant (Global.lookup_constant sp) with
              | Some c -> Declarations.force c
 	     | _ -> assert false)
-       with _ -> assert false)
+       with e when Errors.noncritical e -> assert false)
     |_ -> assert false
 
 let coq_constant s =
@@ -215,13 +214,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
 
 
 
@@ -350,7 +349,8 @@ open Term
 let pr_info f_info =
   str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
     str "function_constant_type := " ++
-    (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
+    (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant))
+     with e when Errors.noncritical e -> mt ()) ++ fnl () ++
     str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
     str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
     str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
@@ -502,22 +502,22 @@ exception ToShow of exn
 let init_constant dir s =
   try
     Coqlib.gen_constant "Function" dir s
-  with e -> raise (ToShow e)
+  with e when Errors.noncritical e -> raise (ToShow e)
 
 let jmeq () =
   try
     (Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
      init_constant ["Logic";"JMeq"] "JMeq")
-  with e -> raise (ToShow e)
+  with e when Errors.noncritical e -> raise (ToShow e)
 
 let jmeq_rec () =
   try
     Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
 	  init_constant ["Logic";"JMeq"] "JMeq_rec"
-  with e -> raise (ToShow e)
+  with e when Errors.noncritical e -> raise (ToShow e)
 
 let jmeq_refl () =
   try
     Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
     init_constant ["Logic";"JMeq"] "JMeq_refl"
-  with e -> raise (ToShow e)
+  with e when Errors.noncritical e -> raise (ToShow e)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 55451a9f..7b5dd763 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -59,14 +59,17 @@ let observennl strm =
 
 
 let do_observe_tac s tac g =
-  let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
+  let goal =
+    try Printer.pr_goal g
+    with e when Errors.noncritical e -> assert false
+  in
   try
     let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
-  with e ->
-    let e' = Cerrors.process_vernac_interp_error e in
+  with reraise ->
+    let e' = Cerrors.process_vernac_interp_error reraise in
     msgnl (str "observation "++ s++str " raised exception " ++
 	     Errors.print e' ++ str " on goal " ++ goal );
-    raise e;;
+    raise reraise;;
 
 
 let observe_tac s tac g =
@@ -568,7 +571,7 @@ let rec reflexivity_with_destruct_cases g =
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
 	| _ -> reflexivity
-    with _ -> reflexivity
+    with e when Errors.noncritical e -> reflexivity
   in
   let eq_ind =     Coqlib.build_coq_eq () in
   let discr_inject =
@@ -862,11 +865,11 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
       funs;
-  with e ->
+  with reraise ->
     (* In case of problem, we reset all the lemmas *)
     Pfedit.delete_all_proofs ();
     States.unfreeze previous_state;
-    raise e
+    raise reraise
 
 
 
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 6ee2f352..bd1a1710 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -70,7 +70,7 @@ let ident_global_exist id =
     let ans = CRef (Libnames.Ident (dummy_loc,id)) in
     let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in
     true
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 (** [next_ident_fresh id] returns a fresh identifier (ie not linked in
     global env) with base [id]. *)
@@ -793,10 +793,10 @@ let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
 
   let params1 =
     try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
-    with _ -> [] in
+    with e when Errors.noncritical e -> [] in
   let params2 =
     try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
-    with _ -> [] in
+    with e when Errors.noncritical e -> [] in
 
   let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
   let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 892c1a77..9853fd73 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -94,11 +94,11 @@ let do_observe_tac s tac g =
     let v = tac g in 
     ignore(Stack.pop debug_queue);
     v
-  with e -> 
+  with reraise ->
     if not (Stack.is_empty debug_queue)
     then
-      print_debug_queue true e;
-    raise e
+      print_debug_queue true reraise;
+    raise reraise
 
 let observe_tac s tac g =
   if Tacinterp.get_debug () <> Tactic_debug.DebugOff
@@ -140,7 +140,7 @@ let def_of_const t =
       (try (match body_of_constant (Global.lookup_constant sp) with
              | Some c -> Declarations.force c
 	     | _ -> assert false)
-       with _ ->
+       with e when Errors.noncritical e ->
 	 anomaly ("Cannot find definition of constant "^
 		    (string_of_id (id_of_label (con_label sp))))
       )
@@ -380,7 +380,11 @@ let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
 		(fun g1 ->
 		   let ty_teq = pf_type_of g1 (mkVar teq) in
 		   let teq_lhs,teq_rhs =
-		     let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in
+		     let _,args =
+                       try destApp ty_teq
+                       with e when Errors.noncritical e ->
+                         Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false
+                     in
 		     args.(1),args.(2)
 		   in
 	           cont_function (mkVar teq::eqs) (Termops.replace_term teq_lhs teq_rhs expr) g1
@@ -701,12 +705,17 @@ let proveterminate nb_arg rec_arg_id is_mes acc_inv (hrec:identifier)
             (match find_call_occs  nb_arg 0 f_constr expr with
 	      _,[] ->
 	      (try observe_tac "base_leaf" (base_leaf func eqs expr)
-	       with e -> (msgerrnl (str "failure in base case");raise e ))
+	       with reraise ->
+                 (msgerrnl (str "failure in base case");raise reraise ))
 	    | _, _::_ ->
 	      observe_tac "rec_leaf"
 	        (rec_leaf is_mes acc_inv hrec func eqs expr)) in
       v
-    with e -> begin msgerrnl(str "failure in proveterminate"); raise e end
+    with reraise ->
+      begin
+        msgerrnl(str "failure in proveterminate");
+        raise reraise
+      end
   in
   proveterminate
 
@@ -931,7 +940,7 @@ let is_rec_res id =
   let id_name = string_of_id id in
   try
     String.sub id_name 0 (String.length rec_res_name) = rec_res_name
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 let clear_goals =
   let rec clear_goal t =
@@ -969,7 +978,8 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     | Some s -> s
     | None   ->
 	try (add_suffix current_proof_name "_subproof")
-	with _ -> anomaly "open_new_goal with an unamed theorem"
+	with e when Errors.noncritical e ->
+          anomaly "open_new_goal with an unamed theorem"
   in
   let sign = initialize_named_context_for_proof () in
   let na = next_global_ident_away name [] in
@@ -1439,7 +1449,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     let stop = ref false in
     begin
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type)
-      with e ->
+      with e when Errors.noncritical e ->
 	begin
 	  if Tacinterp.get_debug () <> Tactic_debug.DebugOff
 	  then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)
@@ -1474,9 +1484,10 @@ 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 ->
+  with reraise ->
     begin
-      (try ignore (Backtrack.backto previous_label) with _ -> ());
+      (try ignore (Backtrack.backto previous_label)
+       with e when Errors.noncritical e -> ());
       (*       anomaly "Cannot create termination Lemma" *)
-      raise e
+      raise reraise
     end
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 25579a87..a5b0da9c 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -331,7 +331,7 @@ let dual_raw_certificate (l:  (Poly.t * Mc.op1) list) =
     | Inr _ -> None
     | Inl cert ->  Some (rats_to_ints (Vect.to_list cert)) 
        (* should not use rats_to_ints *)
-  with x -> 
+  with x when Errors.noncritical x ->
    if debug 
    then (Printf.printf "raw certificate %s" (Printexc.to_string x);   
          flush stdout) ;
@@ -377,8 +377,9 @@ let linear_prover n_spec l  =
 
 
 let linear_prover n_spec l  =
- try linear_prover n_spec l with
-   x -> (print_string (Printexc.to_string x); None)
+ try linear_prover n_spec l
+ with x when x <> Sys.Break ->
+   (print_string (Printexc.to_string x); None)
 
 let linear_prover_with_cert spec l = 
   match linear_prover spec l with
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 2020447f..ff08aeb3 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -937,7 +937,8 @@ struct
                            let (expr,env) = parse_expr env args.(0) in
                            let power = (parse_exp expr args.(1)) in
                              (power  , env)
-			 with _ ->   (* if the exponent is a variable *)
+			 with e when e <> Sys.Break ->
+                           (* if the exponent is a variable *)
                            let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
                        end
                    | Ukn  s ->
@@ -1112,8 +1113,12 @@ struct
   
   let parse_formula parse_atom env tg term =
 
-    let parse_atom env tg t = try let (at,env) = parse_atom env t in
-                                    (A(at,tg,t), env,Tag.next tg) with _ -> (X(t),env,tg) in
+    let parse_atom env tg t =
+      try
+        let (at,env) = parse_atom env t in
+        (A(at,tg,t), env,Tag.next tg)
+      with e when e <> Sys.Break -> (X(t),env,tg)
+    in
 
     let rec xparse_formula env tg term =
      match kind_of_term term with
@@ -1189,7 +1194,8 @@ let same_proof sg cl1 cl2 =
  let rec xsame_proof sg =
   match sg with
    | [] -> true
-   | n::sg -> (try List.nth cl1 n = List.nth cl2 n with _ -> false)
+   | n::sg ->
+     (try List.nth cl1 n = List.nth cl2 n with e when e <> Sys.Break -> false)
       && (xsame_proof sg ) in
   xsame_proof sg
 
@@ -1253,7 +1259,7 @@ let btree_of_array typ a  =
 let btree_of_array typ a =
  try
   btree_of_array typ a
- with x ->
+ with x when x <> Sys.Break ->
   failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x))
 
 let dump_varmap typ env =
@@ -1322,7 +1328,7 @@ let rec parse_hyps parse_arith env tg hyps =
       try
        let (c,env,tg) = parse_formula parse_arith env  tg t in
 	((i,c)::lhyps, env,tg)
-      with _ -> 		(lhyps,env,tg)
+      with e when e <> Sys.Break -> 		(lhyps,env,tg)
        (*(if debug then Printf.printf "parse_arith : %s\n" x);*)
 
 
@@ -1466,7 +1472,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
           (pp_ml_list prover.pp_f) (List.map fst new_cl)   ;
           flush stdout
       end ; *)
-    let res = try prover.compact prf remap with x ->
+    let res = try prover.compact prf remap with x when x <> Sys.Break ->
       if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
       (* This should not happen -- this is the recovery plan... *)
       match prover.prover (List.map fst new_cl) with
@@ -2031,13 +2037,13 @@ let xlia gl =
   try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
       [ linear_Z ] gl
-  with z -> (*Printexc.print_backtrace stdout ;*) raise z
+  with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
 let xnlia gl =
   try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
       [ nlinear_Z ] gl
-  with z -> (*Printexc.print_backtrace stdout ;*) raise z
+  with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
 
 
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index dfda5984..0f26575c 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -150,7 +150,7 @@ let real_nonlinear_prover d l =
    S (Some proof)
  with
   | Sos_lib.TooDeep -> S None
-  |    x        ->   F (Printexc.to_string x)
+  | x when x <> Sys.Break -> F (Printexc.to_string x)
 
 (* This is somewhat buggy, over Z, strict inequality vanish... *)
 let pure_sos  l =
@@ -174,7 +174,7 @@ let pure_sos  l =
     S (Some proof)
  with
 (*   | Sos.CsdpNotFound -> F "Sos.CsdpNotFound" *)
-   |  x        -> (* May be that could be refined *) S None
+   | x when x <> Sys.Break -> (* May be that could be refined *) S None
 
 
 
@@ -203,7 +203,7 @@ let main () =
       Marshal.to_channel  chan (cert:csdp_certificate) [] ;
       flush chan ;
       exit 0
-  with  x -> (Printf.fprintf chan "error %s" (Printexc.to_string x)  ; exit 1)
+  with any -> (Printf.fprintf chan "error %s" (Printexc.to_string any)  ; exit 1)
 
 ;;
 
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index d9201722..6effa4c4 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -728,7 +728,8 @@ struct
 	    try
 	      Some (bound_of_variable IMap.empty fresh s.sys)
 	    with
-		x -> Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None
+	      x when x <> Sys.Break ->
+                Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None
 
 
   let find_point cstrs =
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index ccbf0406..3129e54d 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -29,10 +29,10 @@ let finally f rst =
   try
     let res = f () in
       rst () ; res
-  with x ->
+  with reraise ->
     (try rst ()
-    with _  -> raise x
-    ); raise x
+    with any  -> raise reraise
+    ); raise reraise
 
 let map_option f x =
   match x with
@@ -431,14 +431,16 @@ let command exe_path args vl =
 	    | Unix.WEXITED 0 ->
 		let inch  = Unix.in_channel_of_descr stdout_read in
 		  begin try Marshal.from_channel inch 
-                        with x -> failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) 
+                        with x when x <> Sys.Break ->
+                          failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x))
                   end
 	    | Unix.WEXITED i   -> failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i)
 	    | Unix.WSIGNALED i -> failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i)
 	    | Unix.WSTOPPED i  -> failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i))
         (* Cleanup  *)
 	(fun () ->
-	  List.iter (fun x -> try Unix.close x with _ -> ()) [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write])
+	  List.iter (fun x -> try Unix.close x with e when e <> Sys.Break -> ())
+            [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write])
 
 (* Local Variables: *)
 (* coding: utf-8 *)
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index cb7a9280..6d1a2927 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -82,10 +82,10 @@ let finally f rst =
   try
     let res = f () in
       rst () ; res
-  with x ->
+  with reraise ->
     (try rst ()
-    with _  -> raise x
-    ); raise x
+    with any  -> raise reraise
+    ); raise reraise
 
 
 let read_key_elem inch =
@@ -93,7 +93,7 @@ let read_key_elem inch =
     Some (Marshal.from_channel inch)
   with
     | End_of_file -> None
-    |    _        -> raise InvalidTableFormat
+    | e when e <> Sys.Break -> raise InvalidTableFormat
 
 (** In win32, it seems that we should unlock the exact zone
     that has been locked, and not the whole file *)
@@ -151,7 +151,7 @@ let open_in f =
 	    Table.iter 
 	      (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
 	    flush outch ; 
-	  with  _ -> () )
+	  with e when e <> Sys.Break -> () )
 	    ;
 	    unlock out ; 
 	    { outch = outch ;
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 996dbadd..68fb2626 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -237,7 +237,8 @@ open Format
 
 let getvar lv i =
   try (nth lv i)
-  with _ -> (fold_left (fun r x -> r^" "^x) "lv= " lv)
+  with e when Errors.noncritical e ->
+    (fold_left (fun r x -> r^" "^x) "lv= " lv)
     ^" i="^(string_of_int i)
 
 let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
@@ -590,7 +591,7 @@ let coefpoldep = Hashtbl.create 51
 (* coef of q in p = sum_i c_i*q_i *)
 let coefpoldep_find p q =
   try (Hashtbl.find coefpoldep (p.num,q.num))
-  with _ -> []
+  with Not_found -> []
 
 let coefpoldep_remove p q =
   Hashtbl.remove coefpoldep (p.num,q.num)
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index 0eea961d..fdc8e865 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -173,7 +173,7 @@ let rec equal p q =
 			       then failwith "raté")
 		    p1;
 		  true)
-	     with _ -> false)
+	     with e when Errors.noncritical e -> false)
     | (_,_) -> false
 
 (* normalize polynomial: remove head zeros, coefficients are normalized
@@ -524,7 +524,7 @@ let div_pol_rat p q=
 		   q x in
          (* degueulasse, mais c 'est pour enlever un warning *)
          if s==s then true else true)
-    with _ -> false
+    with e when Errors.noncritical e -> false
 
 (***********************************************************************
   5. Pseudo-division and gcd with subresultants.
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index c16bd425..17c8654b 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -33,10 +33,11 @@ let set_of_list_eq eq l =
 
 let memos s memoire nf f x =
    try (let v = Hashtbl.find memoire (nf x) in pr s;v)
-   with _ -> (pr "#";
-	      let v = f x in
-	      Hashtbl.add memoire (nf x) v;
-	      v)
+   with e when Errors.noncritical e ->
+     (pr "#";
+      let v = f x in
+      Hashtbl.add memoire (nf x) v;
+      v)
 
 
 (**********************************************************************
@@ -64,7 +65,7 @@ let facteurs_liste div constant lp =
                                    if not (constant r)
 				   then l1:=r::(!l1)
                                    else p_dans_lmin:=true)
-			      with _ -> ())
+			      with e when Errors.noncritical e -> ())
                      lmin;
           if !p_dans_lmin
           then factor lmin lp1
@@ -75,7 +76,8 @@ let facteurs_liste div constant lp =
                 List.iter (fun q -> try (let r = div q p in
 					 if not (constant r)
 					 then l1:=r::(!l1))
-				    with _ -> lmin1:=q::(!lmin1))
+				    with e when Errors.noncritical e ->
+                                      lmin1:=q::(!lmin1))
                           lmin;
 	        factor (List.rev (p::(!lmin1))) !l1)
           (* au moins un q de lmin divise p non trivialement *)
@@ -105,7 +107,7 @@ let factorise_tableau div zero c f l1 =
       	                       li:=j::(!li);
                                r:=rr;
 			   done)
-                      with _ -> ())
+                      with e when Errors.noncritical e -> ())
                   l1;
       res.(i)<-(!r,!li))
      f;
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 028ef95d..ffa99fc7 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -885,7 +885,7 @@ let rec transform p t =
     try
       let v,th,_ = find_constr t' in
       [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
-    with _ ->
+    with e when Errors.noncritical e ->
       let v = new_identifier_var ()
       and th = new_identifier () in
       hide_constr t' v th isnat;
@@ -924,7 +924,8 @@ let rec transform p t =
          | _ -> default false t
        end
    | Kapp((Zpos|Zneg|Z0),_) ->
-       (try ([],Oz(recognize_number t)) with _ -> default false t)
+       (try ([],Oz(recognize_number t))
+        with e when Errors.noncritical e -> default false t)
    | Kvar s -> [],Oatom s
    | Kapp(Zopp,[t]) ->
        let tac,t' = transform (P_APP 1 :: p) t in
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index f0ca3bb9..216a719d 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -221,7 +221,10 @@ let compute_rhs bodyi index_of_f =
 (*s Now the function [compute_ivs] itself *)
 
 let compute_ivs gl f cs =
-  let cst = try destConst f with _ -> i_can't_do_that () in
+  let cst =
+    try destConst f
+    with e when Errors.noncritical e -> i_can't_do_that ()
+  in
   let body = Environ.constant_value (Global.env()) cst in
   match decomp_term body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index ae73069d..7b0d96bb 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -292,7 +292,8 @@ let unbox = function
 (* Protects the convertibility test against undue exceptions when using it
    with untyped terms *)
 
-let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false
+let safe_pf_conv_x gl c1 c2 =
+  try pf_conv_x gl c1 c2 with e when Errors.noncritical e -> false
 
 
 (* Add a Ring or a Semi-Ring to the database after a type verification *)
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index e810e15c..fb45e816 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -335,7 +335,7 @@ let parse_term t =
     | Kapp("Z.succ",[t]) -> Tsucc t
     | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) ->
-	(try Tnum (recognize t) with _ -> Tother)
+	(try Tnum (recognize t) with e when Errors.noncritical e -> Tother)
     | _ -> Tother
   with e when Logic.catchable_exception e -> Tother
 
@@ -357,6 +357,6 @@ let is_scalar t =
     | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true
     | _ -> false in
-  try aux t with _ -> false
+  try aux t with e when Errors.noncritical e -> false
 
 end
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 4a6d462e..e57230cb 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -225,7 +225,8 @@ let add_reified_atom t env =
     env.terms <- env.terms @ [t]; i
 
 let get_reified_atom env =
-  try List.nth env.terms with _ -> failwith "get_reified_atom"
+  try List.nth env.terms
+  with e when Errors.noncritical e -> failwith "get_reified_atom"
 
 (* \subsection{Gestion de l'environnement de proposition pour Omega} *)
 (* ajout d'une proposition *)
@@ -235,7 +236,9 @@ let add_prop env t =
     let i = List.length env.props in  env.props <- env.props @ [t]; i
 
 (* accès a une proposition *)
-let get_prop v env = try List.nth v env with _ -> failwith "get_prop"
+let get_prop v env =
+  try List.nth v env
+  with e when Errors.noncritical e -> failwith "get_prop"
 
 (* \subsection{Gestion du nommage des équations} *)
 (* Ajout d'une equation dans l'environnement de reification *)
@@ -247,7 +250,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 +353,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 +385,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 +402,11 @@ let reified_of_omega env body constant =
   List.fold_right mk_coeff body coeff_constant
 
 let reified_of_omega env body c  =
-  begin try
+  try
     reified_of_omega env body c
-  with e ->
-    display_eq display_omega_var (body,c); raise e
-  end
+  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
@@ -1000,10 +1005,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 =
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 956ccf09..6e7a8d32 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -90,7 +90,8 @@ VERNAC COMMAND EXTEND Subtac
 
 let try_catch_exn f e =
   try f e
-  with exn -> errorlabstrm "Program" (Errors.print exn)
+  with exn when Errors.noncritical exn ->
+    errorlabstrm "Program" (Errors.print exn)
 
 let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e
 let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 281e981b..ad248bfb 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -221,6 +221,6 @@ let subtac (loc, command) =
   | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
      Loc.Exc_located (loc, e') as e) -> raise e
 
-  | e -> 
+  | reraise ->
       (*       msg_warning (str "Uncaught exception: " ++ Errors.print e); *)
-      raise e
+      raise reraise
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 221b57ee..0b1ed9bb 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -342,7 +342,7 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
       let pred = predicate 0 c in
       let env' = push_rel_context (context_of_arsign arsign) env in
 	ignore(Typing.sort_of env' evm pred); pred
-    with _ -> lift nar c
+    with e when Errors.noncritical e -> lift nar c
 
 module Cases_F(Coercion : Coercion.S) : S = struct
 
@@ -1465,7 +1465,8 @@ let extract_arity_signatures env0 tomatchl tmsign =
 	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
 	  let arsign = fst (get_arity env0 indf) in
 	    (na,None,build_dependent_inductive env0 indf)
-	    ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign with _ -> assert false) in
+	    ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign
+              with e when Errors.noncritical e -> assert false) in
   let rec buildrec = function
     | [],[] -> []
     | (_,tm)::ltm, x::tmsign ->
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 168a799d..0c03fb4c 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -356,7 +356,7 @@ module Coercion = struct
 		     jres),
 		jres.uj_type)
              (hj,typ_cl) p)
-    with _ -> anomaly "apply_coercion"
+    with e when Errors.noncritical e -> anomaly "apply_coercion"
 
   let inh_app_fun env isevars j =
     let isevars = ref isevars in
@@ -506,5 +506,5 @@ module Coercion = struct
 	    with NoSubtacCoercion ->
 	      error_cannot_coerce env' isevars (t, t'))
 	else isevars
-      with _ -> isevars
+      with e when Errors.noncritical e -> isevars
 end
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 14a09032..537a8301 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -248,7 +248,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	  | [(_, None, t); (_, None, u)], Sort (Prop Null)
 	      when Reductionops.is_conv env !isevars t u -> t
 	  | _, _ -> error ()
-      with _ -> error ()
+      with e when Errors.noncritical e -> error ()
   in
   let measure = interp_casted_constr isevars binders_env measure relargty in
   let wf_rel, wf_rel_fun, measure_fn =
@@ -440,7 +440,7 @@ let interp_recursive fixkind l =
       let sort = Retyping.get_type_of env !evdref t in
       let fixprot =
 	try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|])
-	with e -> t
+	with e when Errors.noncritical e -> t
       in
 	(id,None,fixprot) :: env')
       [] fixnames fixtypes
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index dfcc8526..d8f46098 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -121,7 +121,7 @@ let obl_substitution expand obls deps =
        let xobl = obls.(x) in
        let oblb =
 	 try get_obligation_body expand xobl
-	 with _ -> assert(false)
+	 with e when Errors.noncritical e -> assert(false)
        in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
     deps []
 
@@ -498,7 +498,8 @@ let rec solve_obligation prg num tac =
 		let obls = Array.copy obls in
 		let _ = obls.(num) <- obl in
 		let res = try update_obls prg obls (pred rem)
-		  with e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e))
+		  with e when Errors.noncritical e ->
+                    pperror (Errors.print (Cerrors.process_vernac_interp_error e))
 		in
 		  match res with
 		  | Remain n when n > 0 ->
@@ -552,7 +553,7 @@ and solve_obligation_by_tac prg obls i tac =
 	| Refiner.FailError (_, s) ->
 	    user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
 	| Util.Anomaly _ as e -> raise e
-	| e -> false
+	| e when Errors.noncritical e -> false
 
 and solve_prg_obligations prg ?oblset tac =
   let obls, rem = prg.prg_obligations in
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 95e756ab..f0579711 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -302,7 +302,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | GCoFix i ->
 	      let cofix = (i,(names,ftys,fdefs)) in
-	      (try check_cofix env cofix with e -> Loc.raise loc e);
+	      (try check_cofix env cofix
+               with e when Errors.noncritical e -> Loc.raise loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
@@ -601,7 +602,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	     ~split:true ~fail:true env !evdref;
 	   evdref := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
 	     ~split:true ~fail:false env !evdref
-	 with e -> if fail_evar then raise e else ());
+	 with e when Errors.noncritical e ->
+           if fail_evar then raise e else ());
       evdref := consider_remaining_unif_problems env !evdref;
       let c = if expand_evar then nf_evar !evdref c' else c' in
       if fail_evar then check_evars env Evd.empty !evdref c;
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index fbb44811..e32bb9e0 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -232,7 +232,7 @@ let build_dependent_sum l =
 	let hyptype = substl names t in
 	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
 	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
-	   with _ -> ());
+	   with e when Errors.noncritical e -> ());
 	let tac = assert_tac (Name n) hyptype in
 	let conttac =
 	  (fun cont ->
@@ -331,7 +331,7 @@ let destruct_ex ext ex =
 	       Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 ->
 		 let (dom, rng) =
 		   try (args.(0), args.(1))
-		   with _ -> assert(false)
+		   with e when Errors.noncritical e -> assert(false)
 		 in
 		 let pi1 = (mk_ex_pi1 dom rng acc) in
 		 let rng_body =
@@ -375,9 +375,9 @@ let solve_by_tac evi t =
       Inductiveops.control_only_guard (Global.env ())
 	const.Entries.const_entry_body;
       const.Entries.const_entry_body
-  with e ->
+  with reraise ->
     Pfedit.delete_current_proof();
-    raise e
+    raise reraise
 
 (* let apply_tac t goal = t goal *)
 
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index da0a65ff..a14eda60 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -349,7 +349,7 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
          if computeinnertypes then
 try
           Acic.CicHash.find terms_to_types tt
-with _ ->
+with e when e <> Sys.Break ->
 (*CSC: Warning: it really happens, for example in Ring_theory!!! *)
 Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false
          else
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index a21a919a..c22c16f0 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -147,7 +147,8 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
 (*CSC: universes.                                                        *)
 (try
         Typeops.judge_of_type u
- with _ -> (* Successor of a non universe-variable universe anomaly *)
+ with e when e <> Sys.Break ->
+ (* Successor of a non universe-variable universe anomaly *)
  (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ;
   Typeops.judge_of_type (Termops.new_univ ())
 )
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 1037bbf0..867aac71 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -143,7 +143,7 @@ let rec join_dirs cwd =
   | he::tail ->
       (try
         Unix.mkdir cwd 0o775
-       with _ -> () (* Let's ignore the errors on mkdir *)
+       with e when e <> Sys.Break -> () (* Let's ignore the errors on mkdir *)
       ) ;
      let newcwd = cwd ^ "/" ^ he in
       join_dirs newcwd tail