Merge PR #11774: [exn] [nit] Remove not very useful re-raises.

Reviewed-by: ppedrot

6 files changed, 21 insertions, 47 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 535b7de121..a37d04d82c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1303,12 +1303,7 @@ let start_library dir senv =
     required = senv.required }
 
 let export ?except ~output_native_objects senv dir =
-  let senv =
-    try join_safe_environment ?except senv
-    with e ->
-      let e = Exninfo.capture e in
-      CErrors.user_err ~hdr:"export" (CErrors.iprint e)
-  in
+  let senv = join_safe_environment ?except senv in
   assert(senv.future_cst = []);
   let () = check_current_library dir senv in
   let mp = senv.modpath in
diff --git a/lib/control.ml b/lib/control.ml
index e67e88ee95..1898eab89e 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -75,8 +75,8 @@ let windows_timeout n f x e =
     if not !exited then begin killed := true; raise Sys.Break end
     else raise e
   | e ->
-    let () = killed := true in
     let e = Exninfo.capture e in
+    let () = killed := true in
     Exninfo.iraise e
 
 type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b }
diff --git a/lib/pp.ml b/lib/pp.ml
index 1bd160dcda..f9b6ef20bf 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -201,11 +201,7 @@ let pp_with ft pp =
                                  pp_cmd s;
                                  pp_close_tag ft () [@warning "-3"]
   in
-  try pp_cmd pp
-  with reraise ->
-    let reraise = Exninfo.capture reraise in
-    let () = Format.pp_print_flush ft () in
-    Exninfo.iraise reraise
+  pp_cmd pp
 
 (* If mixing some output and a goal display, please use msg_warning,
    so that interfaces (proofgeneral for example) can easily dispatch
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 7cdfd0637a..a7ba12bb1f 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -120,18 +120,14 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~
   let evd = Evd.from_ctx ctx in
   let goals = [ (Global.env_of_context sign , typ) ] in
   let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
-  try
-    let pf, status = by tac pf in
-    let open Proof_global in
-    let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in
-    match entries with
-    | [entry] ->
-      entry, status, universes
-    | _ ->
-      CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
-  with reraise ->
-    let reraise = Exninfo.capture reraise in
-    Exninfo.iraise reraise
+  let pf, status = by tac pf in
+  let open Proof_global in
+  let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in
+  match entries with
+  | [entry] ->
+    entry, status, universes
+  | _ ->
+    CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
 
 let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac =
   let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index e0afb7f483..5d38ea32be 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -92,28 +92,18 @@ let warn_deprecated_command =
 (* Interpretation of a vernac command *)
 
 let type_vernac opn converted_args ~atts =
-  let phase = ref "Looking up command" in
-  try
-    let depr, callback = vinterp_map opn in
-    let () = if depr then
+  let depr, callback = vinterp_map opn in
+  let () = if depr then
       let rules = Egramml.get_extend_vernac_rule opn in
       let pr_gram = function
-      | Egramml.GramTerminal s -> str s
-      | Egramml.GramNonTerminal _ -> str "_"
+        | Egramml.GramTerminal s -> str s
+        | Egramml.GramNonTerminal _ -> str "_"
       in
       let pr = pr_sequence pr_gram rules in
       warn_deprecated_command pr;
-    in
-    phase := "Checking arguments";
-    let hunk = callback converted_args in
-    phase := "Executing command";
-    hunk ~atts
-  with
-  | reraise ->
-    let reraise = Exninfo.capture reraise in
-    if !Flags.debug then
-      Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase);
-    Exninfo.iraise reraise
+  in
+  let hunk = callback converted_args in
+  hunk ~atts
 
 (** VERNAC EXTEND registering *)
 
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 59557a60a6..280343f315 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -18,12 +18,9 @@ module Parser = struct
 
   let parse ps entry pa =
     Pcoq.unfreeze ps;
-    Flags.with_option Flags.we_are_parsing (fun () ->
-      try Pcoq.Entry.parse entry pa
-      with e when CErrors.noncritical e ->
-        let (e, info) = Exninfo.capture e in
-        Exninfo.iraise (e, info))
-    ()
+    Flags.with_option Flags.we_are_parsing
+      (fun () -> Pcoq.Entry.parse entry pa)
+      ()
 
 end