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

Reviewed-by: ppedrot

2 files changed, 10 insertions, 23 deletions

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