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

7 files changed, 84 insertions, 136 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index f4f62cb85..ac148fe18 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 de20756b3..9b851447c 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 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
 
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c59e43b45..89c6a091a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -892,20 +892,15 @@ let onEquality with_evars tac (c,lbindc) =
   Proofview.Goal.raw_enter begin fun gl ->
   let type_of = pf_type_of gl in
   let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
-  try (* type_of can raise exceptions *)
   let t = type_of c in
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
-  begin try (* clenv_pose_dependent_evars can raise exceptions *)
   let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
   let (eq,eq_args) = find_this_eq_data_decompose gl eqn in
   tclTHEN
-    (Proofview.V82.tactic (Refiner.tclEVARS eq_clause'.evd))
+    (Proofview.V82.tclEVARS eq_clause'.evd)
     (tac (eq,eqn,eq_args) eq_clause')
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 let onNegatedEquality with_evars tac =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b3f33b19c..14555279d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -569,17 +569,13 @@ let interp_auto_lemmas ist env sigma lems =
 let pf_interp_type ist gl =
   interp_type ist (pf_env gl) (project gl)
 
-let new_interp_type ist c =
+let new_interp_type ist c k =
   let open Proofview.Goal in
   let open Proofview.Notations in
-  let interp gl =
-    try
-      let (sigma, c) = interp_type ist (env gl) (sigma gl) c in
-      Proofview.V82.tclEVARS sigma <*> Proofview.tclUNIT c
-    with e when Proofview.V82.catchable_exception e ->
-      Proofview.tclZERO e
-  in
-  interp
+  Proofview.Goal.raw_enter begin fun gl ->
+    let (sigma, c) = interp_type ist (env gl) (sigma gl) c in
+    Proofview.V82.tclEVARS sigma <*> k c
+  end
 
 (* Interprets a reduction expression *)
 let interp_unfold ist env (occs,qid) =
@@ -1473,31 +1469,27 @@ and interp_atomic ist tac =
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-        try (* interp_open_constr_with_bindings_loc can raise exceptions *)
-          let sigma, l =
-            List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
-          in
-          let tac = match cl with
-            | None -> fun l -> Proofview.V82.tactic (Tactics.apply_with_bindings_gen a ev l)
-            | Some cl ->
-                (fun l ->
-                  Proofview.Goal.raw_enter begin fun gl ->
-                    let env = Proofview.Goal.env gl in
-                    let (id,cl) = interp_in_hyp_as ist env cl in
-                    Tactics.apply_in a ev id l cl
-                  end) in
-          Tacticals.New.tclWITHHOLES ev tac sigma l
-        with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+        let sigma, l =
+          List.fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb
+        in
+        let tac = match cl with
+          | None -> fun l -> Proofview.V82.tactic (Tactics.apply_with_bindings_gen a ev l)
+          | Some cl ->
+              (fun l ->
+                Proofview.Goal.raw_enter begin fun gl ->
+                  let env = Proofview.Goal.env gl in
+                  let (id,cl) = interp_in_hyp_as ist env cl in
+                  Tactics.apply_in a ev id l cl
+                end) in
+        Tacticals.New.tclWITHHOLES ev tac sigma l
       end
   | TacElim (ev,cb,cbo) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in 
-        try (* interpretation functions may raise exceptions *)
-          let sigma, cb = interp_constr_with_bindings ist env sigma cb in
-          let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
-          Tacticals.New.tclWITHHOLES ev (Tactics.elim ev cb) sigma cbo
-        with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+        let sigma, cb = interp_constr_with_bindings ist env sigma cb in
+        let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
+        Tacticals.New.tclWITHHOLES ev (Tactics.elim ev cb) sigma cbo
       end
   | TacElimType c ->
       Proofview.V82.tactic begin fun gl -> 
@@ -1561,24 +1553,19 @@ and interp_atomic ist tac =
           gl
       end
   | TacCut c ->
-      let open Proofview.Notations in
-      Proofview.Goal.raw_enter begin fun gl ->
-        new_interp_type ist c gl >>= Tactics.cut
-      end
+      new_interp_type ist c Tactics.cut
   | TacAssert (t,ipat,c) ->
       Proofview.Goal.raw_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-        try (* intrerpreation function may raise exceptions *)
-          let (sigma,c) = 
-            (if Option.is_empty t then interp_constr else interp_type) ist env sigma c
-          in
-          let patt = interp_intro_pattern ist env in
-          Tacticals.New.tclTHEN
-	    (Proofview.V82.tclEVARS sigma)
-            (Tactics.forward (Option.map (interp_tactic ist) t)
-	       (Option.map patt ipat) c)
-        with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+        let (sigma,c) = 
+          (if Option.is_empty t then interp_constr else interp_type) ist env sigma c
+        in
+        let patt = interp_intro_pattern ist env in
+        Tacticals.New.tclTHEN
+          (Proofview.V82.tclEVARS sigma)
+          (Tactics.forward (Option.map (interp_tactic ist) t)
+              (Option.map patt ipat) c)
       end
   | TacGeneralize cl ->
       Proofview.V82.tactic begin fun gl ->
@@ -1617,16 +1604,13 @@ and interp_atomic ist tac =
             (let_tac b (interp_fresh_name ist env na) c_interp clp eqpat)
         else
         (* We try to keep the pattern structure as much as possible *)
-          begin try
-                  let let_pat_tac b na c cl eqpat =
-                    let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
-                    let with_eq = if b then None else Some (true,id) in
-                    Tactics.letin_pat_tac with_eq na c None cl
-                  in
-                  let_pat_tac b (interp_fresh_name ist env na)
-                    (interp_pure_open_constr ist env sigma c) clp eqpat
-            with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-          end
+          let let_pat_tac b na c cl eqpat =
+            let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in
+            let with_eq = if b then None else Some (true,id) in
+            Tactics.letin_pat_tac with_eq na c None cl
+          in
+          let_pat_tac b (interp_fresh_name ist env na)
+            (interp_pure_open_constr ist env sigma c) clp eqpat
       end
 
   (* Automation tactics *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3dd208acb..a2bc37dda 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1295,16 +1295,14 @@ let constructor_tac with_evars expctdnumopt i lbind =
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
     in
-    try (* reduce_to_quantified_ind can raise an exception *)
-      let (mind,redcl) = reduce_to_quantified_ind cl in
-      let nconstr =
-        Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
-      check_number_of_constructors expctdnumopt i nconstr;
-      let cons = mkConstruct (ith_constructor_of_inductive mind i) in
-      let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in
-      (Tacticals.New.tclTHENLIST
-         [Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    let (mind,redcl) = reduce_to_quantified_ind cl in
+    let nconstr =
+      Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
+    check_number_of_constructors expctdnumopt i nconstr;
+    let cons = mkConstruct (ith_constructor_of_inductive mind i) in
+    let apply_tac = Proofview.V82.tactic (general_apply true false with_evars (dloc,(cons,lbind))) in
+    (Tacticals.New.tclTHENLIST
+        [Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); intros; apply_tac])
   end
 
 let one_constructor i lbind = constructor_tac false None i lbind
@@ -1327,13 +1325,11 @@ let any_constructor with_evars tacopt =
     let reduce_to_quantified_ind =
       Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
     in
-  try (* reduce_to_quantified_ind can raise an exception *)
     let mind = fst (reduce_to_quantified_ind cl) in
     let nconstr =
       Array.length (snd (Global.lookup_inductive mind)).mind_consnames in
     if Int.equal nconstr 0 then error "The type has no constructors.";
     tclANY tac (List.interval 1 nconstr)
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
  end
 
 let left_with_bindings  with_evars = constructor_tac with_evars (Some 2) 1
@@ -1429,26 +1425,24 @@ let rewrite_hyp l2r id =
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_type_of gl in
     let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
-    try (* type_of can raise an exception *)
-      let t = whd_betadeltaiota (type_of (mkVar id)) in
-      (* TODO: detect setoid equality? better detect the different equalities *)
-      match match_with_equality_type t with
-      | Some (hdcncl,[_;lhs;rhs]) ->
-          if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then
-	    subst_on l2r (destVar lhs) rhs
-          else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then
-	    subst_on l2r (destVar rhs) lhs
-          else
-	    Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
-      | Some (hdcncl,[c]) ->
-          let l2r = not l2r in (* equality of the form eq_true *)
-          if isVar c then
-	    Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (Proofview.V82.tactic (clear_var_and_eq c))
-          else
-	    Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
-      | _ ->
-          Proofview.tclZERO (Errors.UserError ("",Pp.str"Cannot find a known equation."))
-    with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+    let t = whd_betadeltaiota (type_of (mkVar id)) in
+    (* TODO: detect setoid equality? better detect the different equalities *)
+    match match_with_equality_type t with
+    | Some (hdcncl,[_;lhs;rhs]) ->
+        if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then
+          subst_on l2r (destVar lhs) rhs
+        else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then
+          subst_on l2r (destVar rhs) lhs
+        else
+          Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
+    | Some (hdcncl,[c]) ->
+        let l2r = not l2r in (* equality of the form eq_true *)
+        if isVar c then
+          Tacticals.New.tclTHEN (rew_on l2r allHypsAndConcl) (Proofview.V82.tactic (clear_var_and_eq c))
+        else
+          Tacticals.New.tclTHEN (rew_on l2r onConcl) (Proofview.V82.tactic (tclTRY (clear [id])))
+    | _ ->
+        Proofview.tclZERO (Errors.UserError ("",Pp.str"Cannot find a known equation."))
   end
 
 let rec explicit_intro_names = function
@@ -1906,12 +1900,8 @@ let forward usetac ipat c =
   match usetac with
   | None ->
       Proofview.Goal.raw_enter begin fun gl ->
-      let type_of = Tacmach.New.pf_type_of gl in
-      begin try (* type_of can raise an exception *)
-              let t = type_of c in
-              Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c))
-        with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-      end
+      let t = Tacmach.New.pf_type_of gl  c in
+      Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c))
       end
   | Some tac ->
       Tacticals.New.tclTHENFIRST (assert_as true ipat c) tac
@@ -2117,7 +2107,6 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
   Proofview.Goal.enter begin fun gl ->
   let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
   let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in
-  try (* reduce_to_quantified_ref can raise an exception *)
   let typ0 =  reduce_to_quantified_ref indref tmptyp0 in
   let prods, indtyp = decompose_prod typ0 in
   let argl = snd (decompose_app indtyp) in
@@ -2157,7 +2146,6 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
     end
   in
   atomize_one (List.length argl) params
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 let find_atomic_param_of_ind nparams indtyp =
@@ -3158,7 +3146,6 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n
   let reduce_to_quantified_ref =
     Tacmach.New.pf_apply reduce_to_quantified_ref gl
   in
-  try (* reduce_to_quantified_ref can raise an exception *)
   let typ0 = reduce_to_quantified_ref indref tmptyp0 in
   let indvars = find_atomic_param_of_ind nparams ((strip_prod typ0)) in
   let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [
@@ -3168,7 +3155,6 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n
   ]) in
   apply_induction_in_context
     (Some (hyp0,inhyps)) elim indvars names induct_tac
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps =
@@ -3284,7 +3270,6 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
 	    | _ ->
                 Proofview.Goal.raw_enter begin fun gl ->
                 let type_of = Tacmach.New.pf_type_of gl in
-		try (* type_of can raise an exception *)
                 let x =
 		  id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
 
@@ -3295,7 +3280,6 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
 		Tacticals.New.tclTHEN
 		  (letin_tac None (Name id) c None allHypsAndConcl)
 		  (atomize_list newl')
-                with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e 
                 end in
   Tacticals.New.tclTHENLIST
     [
@@ -3522,9 +3506,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 let symmetry_in id =
   Proofview.Goal.raw_enter begin fun gl ->
-  let type_of = Tacmach.New.pf_type_of gl in
-  try (* type_of can raise an exception *)
-  let ctype = type_of (mkVar id) in
+  let ctype = Tacmach.New.pf_type_of gl (mkVar id) in
   let sign,t = decompose_prod_assum ctype in
   Proofview.tclORELSE
     begin
@@ -3541,7 +3523,6 @@ let symmetry_in id =
       | NoEquationFound -> Hook.get forward_setoid_symmetry_in id
       | e -> Proofview.tclZERO e
     end
-  with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
   end
 
 let intros_symmetry =
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 3c62e2a11..04d0f3de4 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."))