From 4ba8fabb14256cdc65e8440362d6697d9e97b7f4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 1 Mar 2020 02:49:04 -0500
Subject: [exn] [nit] Remove not very useful re-raises.

Cleanup: IMHO most of the re-raises here are not worth it.
---
 tactics/pfedit.ml | 20 ++++++++------------
 1 file changed, 8 insertions(+), 12 deletions(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3