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


From 8bc79fd74ff347d93758ca5c088b085f721819fb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 12 May 2020 12:58:35 +0200
Subject: Remove useless try-with clauses in newring.

This is already protected by then enter block.
---
 plugins/setoid_ring/newring.ml | 32 ++++++++++++++------------------
 1 file changed, 14 insertions(+), 18 deletions(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 633cdbd735..e7c75e029e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -690,15 +690,13 @@ let ring_lookup (f : Value.t) lH rl t =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
-    try (* find_ring_strucure can raise an exception *)
-      let rl = make_args_list sigma rl t in
-      let evdref = ref sigma in
-      let e = find_ring_structure env sigma rl in
-      let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
-      let lH = carg (make_hyp_list env evdref lH) in
-      let ring = ltac_ring_structure e in
-      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    let rl = make_args_list sigma rl t in
+    let evdref = ref sigma in
+    let e = find_ring_structure env sigma rl in
+    let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
+    let lH = carg (make_hyp_list env evdref lH) in
+    let ring = ltac_ring_structure e in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
   end
 
 (***********************************************************************)
@@ -984,13 +982,11 @@ let field_lookup (f : Value.t) lH rl t =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
-    try
-      let rl = make_args_list sigma rl t in
-      let evdref = ref sigma in
-      let e = find_field_structure env sigma rl in
-      let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
-      let lH = carg (make_hyp_list env evdref lH) in
-      let field = ltac_field_structure e in
-      Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    let rl = make_args_list sigma rl t in
+    let evdref = ref sigma in
+    let e = find_field_structure env sigma rl in
+    let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
+    let lH = carg (make_hyp_list env evdref lH) in
+    let field = ltac_field_structure e in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
   end
-- 
cgit v1.2.3