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

1 files changed, 2 insertions, 6 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 3c62e2a11a..04d0f3de4b 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -411,10 +411,8 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
   let rec aux l1 l2 =
     match (l1,l2) with
     | (t1::q1,t2::q2) ->
-        Proofview.Goal.enter begin fun gl ->
-        let type_of = Tacmach.New.pf_type_of gl in
-        begin try (* type_of can raise an exception *)
-        let tt1 = type_of t1 in
+        Proofview.Goal.raw_enter begin fun gl ->
+        let tt1 = Tacmach.New.pf_type_of gl t1 in
         if eq_constr t1 t2 then aux q1 q2
         else (
           let u,v = try  destruct_ind tt1
@@ -454,8 +452,6 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
                   aux q1 q2 ]
               )
         )
-          with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-        end
         end
     | ([],[]) -> Proofview.tclUNIT ()
     | _ -> Proofview.tclZERO (UserError ("" , str"Both side of the equality must have the same arity."))