Removing useless try-with clauses in Goal.enter variants.

1 files changed, 14 insertions, 18 deletions

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 0cb9d4460..df1c77bf1 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -797,17 +797,15 @@ let ltac_ring_structure e =
    lemma1;lemma2;pretac;posttac]
 
 let ring_lookup (f:glob_tactic_expr) lH rl t =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    try (* find_ring_strucure can raise an exception *)
-      let rl = make_args_list rl t in
-      let e = find_ring_structure env sigma rl in
-      let rl = carg (make_term_list e.ring_carrier rl) in
-      let lH = carg (make_hyp_list env lH) in
-      let ring = ltac_ring_structure e in
-      ltac_apply f (ring@[lH;rl])
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    let rl = make_args_list rl t in
+    let e = find_ring_structure env sigma rl in
+    let rl = carg (make_term_list e.ring_carrier rl) in
+    let lH = carg (make_hyp_list env lH) in
+    let ring = ltac_ring_structure e in
+    ltac_apply f (ring@[lH;rl])
   end
 
 TACTIC EXTEND ring_lookup
@@ -1122,17 +1120,15 @@ let ltac_field_structure e =
    field_simpl_eq_in_ok;cond_ok;pretac;posttac]
 
 let field_lookup (f:glob_tactic_expr) lH rl t =
-  Proofview.Goal.enter begin fun gl ->
+  Proofview.Goal.raw_enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    try
-      let rl = make_args_list rl t in
-      let e = find_field_structure env sigma rl in
-      let rl = carg (make_term_list e.field_carrier rl) in
-      let lH = carg (make_hyp_list env lH) in
-      let field = ltac_field_structure e in
-      ltac_apply f (field@[lH;rl])
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    let rl = make_args_list rl t in
+    let e = find_field_structure env sigma rl in
+    let rl = carg (make_term_list e.field_carrier rl) in
+    let lH = carg (make_hyp_list env lH) in
+    let field = ltac_field_structure e in
+    ltac_apply f (field@[lH;rl])
   end