diff options
| author | Pierre-Marie Pédrot | 2020-05-12 11:50:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-12 11:52:04 +0200 |
| commit | e802f48faf7a472000e218c7a3321c10c2171e0f (patch) | |
| tree | a71008833307f5f0278d4f59201bcba9cf8e9690 /plugins | |
| parent | 007ed9e21f69a157ffff3fa5f990f62ab2756416 (diff) | |
Remove useless try-with blocks in congruence.
The inner body was not raising any exception since it was in the monad,
and even if it did so, the enter block would have caught it.
Diffstat (limited to 'plugins')
| -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 |