diff options
| author | Emilio Jesus Gallego Arias | 2020-05-13 02:49:27 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-13 02:49:27 +0200 |
| commit | 4a5944448e31022593df7d6e7e0318cfea92ea98 (patch) | |
| tree | 643d10e4058af9db9efbf84d7c91c4d8eeb152e1 /plugins/cc | |
| parent | 0992c2669324a2ab911f5a4c08c27dc97f2bf371 (diff) | |
| parent | c5fdfe6ffef15795ecfde8f18f332ddefd35605e (diff) | |
Merge PR #12307: Cleaning up the legacy proof engine
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0c305d09e8..c485c38009 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -290,7 +290,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c) let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check (EConstr.of_constr c) | SymAx c -> @@ -350,7 +349,6 @@ let rec proof_tac p : unit Proofview.tactic = app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tacticals.New.tclTHEN injt (proof_tac prf)))) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end let refute_tac c t1 t2 p = @@ -508,11 +506,9 @@ let f_equal = let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let cut_eq c1 c2 = - try (* type_of can raise an exception *) Tacticals.New.tclTHENS (mk_eq _eq c1 c2 Tactics.cut) [Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)] - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE begin match EConstr.kind sigma concl with |