diff --git a/boot/util.ml b/boot/util.ml
index 395bf72815f2..86342e742206 100644
--- a/boot/util.ml
+++ b/boot/util.ml
@@ -10,7 +10,7 @@
 
 let parse_env_line l =
   try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value))
-  with _ -> None
+  with Scanf.Scan_failure _ | End_of_file -> None
 
 let with_ic file f =
   let ic = open_in file in
diff --git a/checker/check.ml b/checker/check.ml
index c7b575fae542..3e0d3cfa7ffd 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -312,7 +312,7 @@ let marshal_in_segment (type a) ~validate ~value ~(segment : a ObjFile.segment)
         let digest = Digest.input ch in
         let () = if not (String.equal digest segment.ObjFile.hash) then raise_notrace Exit in
         v
-      with _ ->
+      with exn when CErrors.noncritical exn ->
         CErrors.user_err (str "Corrupted file " ++ quote (str f))
     in
     let () = Validate.validate value v in
diff --git a/checker/checker.ml b/checker/checker.ml
index cabdcc1af889..26b390bd389e 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -55,7 +55,7 @@ let get_version () =
     let rev = input_line ch in
     let () = close_in ch in
     Printf.sprintf "%s (%s)" ver rev
-  with _ -> Coq_config.version
+  with Sys_error _ | End_of_file -> Coq_config.version
 
 let print_header () =
   Printf.printf "Welcome to Chicken %s\n%!" (get_version ())
diff --git a/clib/terminal.ml b/clib/terminal.ml
index 00945f750721..3d114227cb0a 100644
--- a/clib/terminal.ml
+++ b/clib/terminal.ml
@@ -312,7 +312,7 @@ let parse s =
         let attrs = List.map int_of_string attrs in
         let attrs = parse_style (make ()) attrs in
         (name, attrs) :: accu
-      with _ -> accu
+      with Failure _ | Invalid_argument _ -> accu
     in
     accu
   | _ -> accu
diff --git a/engine/termops.ml b/engine/termops.ml
index 67001f988cc7..98b1ac5ea678 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -88,7 +88,10 @@ module Internal = struct
 
   let protect f x =
     try f x
-    with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
+    with e when
+        (* maybe should be just "not is_interrupted"? *)
+        CErrors.noncritical e || !Flags.in_debugger ->
+      str "EXCEPTION: " ++ str (Printexc.to_string e)
 
   let print_kconstr env sigma a =
     protect (fun c -> print_constr_env env sigma c) a
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 7c25fcc92482..cf184566d1a5 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -43,7 +43,7 @@ let () = at_exit (fun () ->
         let d = Lazy.force my_temp_dir in
         Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d);
         Unix.rmdir d
-      with e ->
+      with (Unix.Unix_error _ | Sys_error _) as e ->
         Feedback.msg_warning
           Pp.(str "Native compile: failed to cleanup: " ++
               str(Printexc.to_string e) ++ fnl()))
diff --git a/lib/envars.ml b/lib/envars.ml
index 3f1d024d2695..ab490b340801 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -14,7 +14,7 @@ open Util
 
 let parse_env_line l =
   try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value))
-  with _ -> None
+  with Scanf.Scan_failure _ | End_of_file -> None
 
 let with_ic file f =
   let ic = open_in file in
diff --git a/lib/spawn.ml b/lib/spawn.ml
index ada7b36130b2..35c5f8cd9f05 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -147,7 +147,7 @@ let spawn_with_control prefer_sock env prog args =
 let output_death_sentence pid oob_req =
   prerr_endline ("death sentence for " ^ pid);
   try output_value oob_req ReqDie; flush oob_req
-  with e -> prerr_endline ("death sentence: " ^ Printexc.to_string e)
+  with e when CErrors.noncritical e -> prerr_endline ("death sentence: " ^ Printexc.to_string e)
 
 (* spawn a process and read its output asynchronously *)
 module Async(ML : MainLoopModel) = struct
@@ -182,7 +182,7 @@ let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) =
     Option.iter close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid Sys.sigkill;
     p.watch <- None
-  with e -> prerr_endline ("kill: "^Printexc.to_string e) end
+  with e when CErrors.noncritical e -> prerr_endline ("kill: "^Printexc.to_string e) end
 
 let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
     prog args callback
@@ -249,7 +249,7 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) =
     Option.iter close_in_noerr oob_resp;
     Option.iter close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid Sys.sigkill;
-  with e -> prerr_endline ("kill: "^Printexc.to_string e) end
+  with e when CErrors.noncritical e -> prerr_endline ("kill: "^Printexc.to_string e) end
 
 let rec wait p =
   (* On windows kill is not reliable, so wait may never return. *)
diff --git a/lib/system.ml b/lib/system.ml
index e6085d8b136d..8f1315c159cb 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -74,7 +74,7 @@ let apply_subdir f path name =
     | Unix.S_REG -> f (FileRegular name)
     | _ -> ()
 
-let readdir dir = try Sys.readdir dir with any -> [||]
+let readdir dir = try Sys.readdir dir with Sys_error _ -> [||]
 
 let process_directory f path =
   Array.iter (apply_subdir f path) (readdir path)
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 4524caffb68d..2cf6ce27a4d4 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -69,7 +69,7 @@ let update_bpt fname offset opt =
           (try
             let p = Loadpath.find_load_path (CUnix.physical_path_of_string dirname) in
             DirPath.repr (Loadpath.logical p)
-          with _ -> []))
+          with exn when CErrors.noncritical exn -> []))
     end
   in
   let dirpath = DirPath.to_string dp in
@@ -170,14 +170,14 @@ let cvt_loc loc =
              let knlen = String.length text in
              let lastdot = String.rindex text '.' in
              String.sub text (lastdot+1) (knlen - (lastdot + 1))
-           with _ -> text
+           with exn when CErrors.noncritical exn -> text
          in
          Printf.sprintf "%s:%d, %s  (%s)" routine line_nb file module_name;
        | Some { fname=ToplevelInput; line_nb } ->
          let items = String.split_on_char '.' text in
          Printf.sprintf "%s:%d, %s" (List.nth items 1) line_nb (List.hd items);
        | _ -> text
-   with _ -> text
+   with exn when CErrors.noncritical exn -> text
 
 let format_stack s =
   List.map (fun (tac, loc) ->
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 195b3ce40546..3765ee43c3a2 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1972,11 +1972,7 @@ Tacticals.tclTHEN
                   ( EConstr.mkVar goal_name
                   , arith_args @ List.map EConstr.mkVar ids )))
       with
-      | CsdpNotFound -> fail_csdp_not_found ()
-      | x ->
-        if debug then
-          Tacticals.tclFAIL (Pp.str (Printexc.get_backtrace ()))
-        else raise x)
+      | CsdpNotFound -> fail_csdp_not_found ())
 
 let micromega_wit_gen pre_process cnf spec prover wit_id ff =
   Proofview.Goal.enter (fun gl ->
@@ -1998,12 +1994,7 @@ let micromega_wit_gen pre_process cnf spec prover wit_id ff =
           let tres' = EConstr.mkApp (Lazy.force coq_list, [|spec.proof_typ|]) in
           Tactics.letin_tac
             None (Names.Name wit_id) res' (Some tres') Locusops.nowhere
-      with
-      | CsdpNotFound -> fail_csdp_not_found ()
-      | x ->
-        if debug then
-          Tacticals.tclFAIL (Pp.str (Printexc.get_backtrace ()))
-        else raise x)
+      with CsdpNotFound -> fail_csdp_not_found ())
 
 let micromega_order_changer cert env ff =
   (*let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *)
@@ -2127,8 +2118,7 @@ let micromega_genr prover tac =
                 [ Generalize.generalize (List.map EConstr.mkVar ids)
                 ; Tactics.exact_check
                     (EConstr.applist (EConstr.mkVar goal_name, arith_args)) ] ]
-      with
-      | CsdpNotFound -> fail_csdp_not_found ())
+      with CsdpNotFound -> fail_csdp_not_found ())
 
 let lift_ratproof prover l =
   match prover l with
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index b9a55a4b504d..39521ee387c1 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -360,10 +360,11 @@ let command exe_path args vl =
       | Unix.WEXITED 0 -> (
         let inch = Unix.in_channel_of_descr stdout_read in
         try Marshal.from_channel inch
-        with any ->
+        with (End_of_file | Failure _) as exn ->
           failwith
-            (Printf.sprintf "command \"%s\" exited %s" exe_path
-               (Printexc.to_string any)) )
+            (Printf.sprintf "command \"%s\" exited with code 0 but result could not be read back: %s"
+               exe_path
+               (Printexc.to_string exn)) )
       | Unix.WEXITED i ->
         failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i)
       | Unix.WSIGNALED i ->
@@ -373,7 +374,7 @@ let command exe_path args vl =
     (* Cleanup  *)
       (fun () ->
       List.iter
-        (fun x -> try Unix.close x with any -> ())
+        (fun x -> try Unix.close x with Unix.Unix_error _ -> ())
         [ stdin_read
         ; stdin_write
         ; stdout_read
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index a3906dd299eb..d5c40961c773 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -795,8 +795,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
    loop ty [] sigma m
 
 let dependent_apply_error =
-  try CErrors.user_err (Pp.str "Could not fill dependent hole in \"apply\"")
-  with err -> err
+  CErrors.UserError (Pp.str "Could not fill dependent hole in \"apply\"")
 
 (* TASSI: Sometimes Coq's apply fails. According to my experience it may be
  * related to goals that are products and with beta redexes. In that case it
diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
index 41920e926122..99e72a714401 100644
--- a/sysinit/coqinit.ml
+++ b/sysinit/coqinit.ml
@@ -120,7 +120,7 @@ let print_memory_stat () =
     let oc = open_out fn in
     Gc.print_stat oc;
     close_out oc
-  with _ -> ()
+  with exn when CErrors.noncritical exn -> ()
 
 let init_load_paths opts =
   let open Coqargs in
diff --git a/tools/configure/util.ml b/tools/configure/util.ml
index 6026fa52cfbb..79764c30cb28 100644
--- a/tools/configure/util.ml
+++ b/tools/configure/util.ml
@@ -172,7 +172,7 @@ let is_executable f =
 (** Equivalent of rm -f *)
 
 let safe_remove f =
-  try Unix.chmod f 0o644; Sys.remove f with _ -> ()
+  try Unix.chmod f 0o644; Sys.remove f with Unix.Unix_error _ | Sys_error _ -> ()
 
 (** The PATH list for searching programs *)
 
@@ -233,4 +233,7 @@ let write_config_file ~file ?(bin=false) action =
     action o;
     close_out o;
     Unix.chmod file 0o444
-  with _ -> close_out o; safe_remove file
+  with exn ->
+    close_out o;
+    safe_remove file;
+    raise exn
diff --git a/toplevel/common_compile.ml b/toplevel/common_compile.ml
index 5ec70808ac9a..e82424c93eff 100644
--- a/toplevel/common_compile.ml
+++ b/toplevel/common_compile.ml
@@ -30,7 +30,7 @@ let ensure_ext ext f =
   end
 
 let safe_chop_extension f =
-  try Filename.chop_extension f with _ -> f
+  try Filename.chop_extension f with Invalid_argument _ -> f
 
 let ensure_bname src tgt =
   let src, tgt = Filename.basename src, Filename.basename tgt in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a0f51f600522..0432d39f834a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -26,7 +26,7 @@ let get_version ~boot =
     let rev = input_line ch in
     let () = close_in ch in
     Printf.sprintf "%s (%s)" ver rev
-  with _ -> Coq_config.version
+  with Sys_error _ | End_of_file -> Coq_config.version
 
 let print_header ~boot () =
   Feedback.msg_info (str "Welcome to Coq " ++ str (get_version ~boot));
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index a4bc88feff10..f699f2cb780f 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -119,7 +119,7 @@ let alarm what internal msg =
 
 let try_declare_scheme ?locmap what f internal names kn =
   try f ?locmap names kn
-  with e ->
+  with e when CErrors.noncritical e ->
   let e = Exninfo.capture e in
   let rec extract_exn = function Logic_monad.TacticFailure e -> extract_exn e | e -> e in
   let msg = match extract_exn (fst e) with
@@ -168,10 +168,9 @@ let try_declare_scheme ?locmap what f internal names kn =
     | InternalDependencies ->
          alarm what internal
            (strbrk "Inductive types with internal dependencies in constructors not supported.")
-    | e when CErrors.noncritical e ->
+    | e ->
         alarm what internal
           (str "Unexpected error during scheme creation: " ++ CErrors.print e)
-    | _ -> Exninfo.iraise e
   in
   match msg with
   | None -> ()
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 5215c9fcfd5f..75f4595851d4 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -270,7 +270,7 @@ let make_style_stack () =
     | Format.String_tag tag ->
       let (tpfx, _) = split_tag tag in
       if tpfx = start_pfx then "" else begin
-        if tpfx = end_pfx then diff_tag_stack := (try List.tl !diff_tag_stack with tl -> []);
+        if tpfx = end_pfx then diff_tag_stack := (match !diff_tag_stack with _ :: tl -> tl | [] -> []);
         match !style_stack with
         | []       -> (* Something went wrong, we fallback *)
           Terminal.eval default_style