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

3 files changed, 15 insertions, 23 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index f4f62cb852..ac148fe182 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -246,7 +246,6 @@ let _M =mkMeta
 let rec proof_tac p : unit Proofview.tactic =
   Proofview.Goal.enter begin fun gl ->
   let type_of = Tacmach.New.pf_type_of gl in
-  try (* type_of can raise exceptions *)
   match p.p_rule with
       Ax c -> Proofview.V82.tactic (exact_check c)
     | SymAx c ->
@@ -315,7 +314,6 @@ let rec proof_tac p : unit Proofview.tactic =
 	 let injt=
 	   mkApp (Lazy.force _f_equal,[|intype;outtype;proj;ti;tj;_M 1|]) in
 	   Tacticals.New.tclTHEN (Proofview.V82.tactic (refine injt)) (proof_tac prf)
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 let refute_tac c t1 t2 p =
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index de20756b3c..9b851447c2 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1825,9 +1825,7 @@ let destructure_hyps =
 	  end
     in
     let hyps = Proofview.Goal.hyps gl in
-    try (* type_of can raise exceptions *)
-      loop hyps
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    loop hyps
   end
 
 let destructure_goal =
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 0cb9d4460f..df1c77bf17 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