From e802f48faf7a472000e218c7a3321c10c2171e0f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 11:50:45 +0200
Subject: 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.
---
 plugins/cc/cctac.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'plugins')

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