diff options
| author | Emilio Jesus Gallego Arias | 2020-03-01 02:49:04 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-08 00:44:58 -0500 |
| commit | 4ba8fabb14256cdc65e8440362d6697d9e97b7f4 (patch) | |
| tree | 6dc6168679e8b48127decd32823afa39ac77355c /tactics | |
| parent | dbd3a4c4213b3d56908a8387de93e27aaec501a4 (diff) | |
[exn] [nit] Remove not very useful re-raises.
Cleanup: IMHO most of the re-raises here are not worth it.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/pfedit.ml | 20 |
1 files changed, 8 insertions, 12 deletions
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 |