diff options
| author | Pierre-Marie Pédrot | 2020-03-10 08:36:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-10 08:36:05 +0100 |
| commit | fea01ea28b9fdfd9fb5be91aba982710f55c3aba (patch) | |
| tree | 1fce7949fabdb4eb17a0627c94d3c611dfd34614 /tactics | |
| parent | bab342d98d413a2b7a20da98c8dbec7616f54bce (diff) | |
| parent | 4ba8fabb14256cdc65e8440362d6697d9e97b7f4 (diff) | |
Merge PR #11774: [exn] [nit] Remove not very useful re-raises.
Reviewed-by: ppedrot
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 |