Replacing catchable_exception by noncritical in try-with blocks.

7 files changed, 21 insertions, 24 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index fbc64d95d0..28dcb00384 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -129,7 +129,7 @@ let find_class_proof proof_type proof_method env evars carrier relation =
     let evars', c = Typeclasses.resolve_one_typeclass env (goalevars evars) goal in
       if extends_undefined (goalevars evars) evars' then raise Not_found
       else app_poly_check env (evars',cstrevars evars) proof_method [| carrier; relation; c |]
-  with e when Logic.catchable_exception e -> raise Not_found
+  with e when CErrors.noncritical e -> raise Not_found
 
 (** Utility functions *)
 
@@ -724,8 +724,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs)
     let rew = if l2r then rew else symmetry env sort rew in
     Some rew
   with
-  | e when Class_tactics.catchable e -> None
-  | Reduction.NotConvertible -> None
+  | e when noncritical e -> None
 
 let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t =
   try
@@ -741,8 +740,7 @@ let unify_abs (car, rel, prf, c1, c2) l2r sort env (sigma, cstrs) t =
     let rew = if l2r then rew else symmetry env sort rew in
     Some rew
   with
-  | e when Class_tactics.catchable e -> None
-  | Reduction.NotConvertible -> None
+  | e when noncritical e -> None
 
 type rewrite_flags = { under_lambdas : bool; on_morphisms : bool }
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 4dc2ade7a1..2fca83f7c6 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -363,7 +363,7 @@ let intern_typed_pattern ist ~as_type ~ltacvars p =
 let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
   let interp_ref r =
     try Inl (intern_evaluable ist r)
-    with e when Logic.catchable_exception e ->
+    with e when CErrors.noncritical e ->
       (* Compatibility. In practice, this means that the code above
          is useless. Still the idea of having either an evaluable
          ref or a pattern seems interesting, with "head" reduction
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 118db01ecb..1e46e1860f 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -25,7 +25,6 @@ open EConstr
 open Tacticals.New
 open Tacmach.New
 open Tactics
-open Logic
 open Libnames
 open Nametab
 open Contradiction
@@ -971,7 +970,7 @@ let rec transform sigma p t =
        tac @ tac', t''
    | Kapp(Z_of_nat,[t']) -> default true t'
    | _ -> default false t
-  with e when catchable_exception e -> default false t
+  with e when noncritical e -> default false t
 
 let shrink_pair p f1 f2 =
   match f1,f2 with
@@ -1420,7 +1419,7 @@ let destructure_omega env sigma tac_def (id,c) =
           normalize_equation sigma
             id INEQ (Lazy.force coq_Zgt_left) 2 t t1 t2 tac_def
       | _ -> tac_def
-    with e when catchable_exception e -> tac_def
+    with e when noncritical e -> tac_def
 
 let reintroduce id =
   (* [id] cannot be cleared if dependent: protect it by a try *)
@@ -1527,7 +1526,7 @@ let nat_inject =
                 Kapp(S,[t]) -> is_number t
               | Kapp(O,[]) -> true
               | _ -> false
-            with e when catchable_exception e -> false
+            with e when noncritical e -> false
           in
           let rec loop p t : unit Proofview.tactic =
             try match destructurate_term sigma t with
@@ -1538,7 +1537,7 @@ let nat_inject =
                         ((Lazy.force coq_inj_S),[t]))
                      (loop (P_APP 1 :: p) t))
               | _ -> explore p t
-            with e when catchable_exception e -> explore p t
+            with e when noncritical e -> explore p t
           in
           if is_number t' then focused_simpl p else loop p t
       | Kapp(Pred,[t]) ->
@@ -1551,7 +1550,7 @@ let nat_inject =
             (explore p t_minus_one)
       | Kapp(O,[]) -> focused_simpl p
       | _ -> Proofview.tclUNIT ()
-    with e when catchable_exception e -> Proofview.tclUNIT ()
+    with e when noncritical e -> Proofview.tclUNIT ()
 
   and loop = function
     | [] -> Proofview.tclUNIT ()
@@ -1615,7 +1614,7 @@ let nat_inject =
                   ]
                 else loop lit
             | _ -> loop lit
-          with e when catchable_exception e -> loop lit end
+          with e when noncritical e -> loop lit end
   in
   let hyps_types = Tacmach.New.pf_hyps_types gl in
   loop (List.rev hyps_types)
@@ -1725,7 +1724,7 @@ let destructure_hyps =
                 (assert_by (Name hid) hty reflexivity)
                 (loop (LocalAssum (make_annot hid Sorts.Relevant, hty) :: lit))
            | _ -> loop lit
-         with e when catchable_exception e -> loop lit
+         with e when noncritical e -> loop lit
        end
     | decl :: lit -> (* variable without body (or !letin_flag isn't set) *)
        let i = NamedDecl.get_id decl in
@@ -1857,7 +1856,7 @@ let destructure_hyps =
           | _ -> loop lit
             with
             | Undecidable -> loop lit
-            | e when catchable_exception e -> loop lit
+            | e when noncritical e -> loop lit
           end
     in
     let hyps = Proofview.Goal.hyps gl in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7393454ba9..9804d4754d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -563,7 +563,7 @@ let apply_special_clear_request clear_flag f =
       let (sigma, (c, bl)) = f env sigma in
       apply_clear_request clear_flag (use_clear_hyp_by_default ()) c
     with
-      e when catchable_exception e -> tclIDTAC
+      e when noncritical e -> tclIDTAC
   end
 
 type multi =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 731792e34e..9d9616354b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -923,7 +923,7 @@ let make_resolve_hyp env sigma decl =
        (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
     | Failure _ -> []
-    | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp.")
+    | e when noncritical e -> anomaly (Pp.str "make_resolve_hyp.")
 
 (* REM : in most cases hintname = id *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ef50c56dc4..123a7feb90 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -853,7 +853,7 @@ let change_on_subterm ~check cv_pb deep t where env sigma c =
   let sigma = if !mayneedglobalcheck then
     begin
       try fst (Typing.type_of env sigma c)
-      with e when catchable_exception e ->
+      with e when noncritical e ->
         error "Replacement would lead to an ill-typed term."
     end else sigma
   in
@@ -1313,7 +1313,7 @@ let cut c =
     (* Backward compat: ensure that [c] is well-typed. Plus we need to
        know the relevance *)
     match Typing.sort_of env sigma c with
-    | exception e when Pretype_errors.precatchable_exception e ->
+    | exception e when noncritical e ->
       Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
     | sigma, s ->
       let r = Sorts.relevance_of_sort s in
@@ -1717,7 +1717,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
         if n<0 then error "Applied theorem does not have enough premises.";
         let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
         Clenvtac.res_pf clause ~with_evars ~flags
-      with exn when catchable_exception exn ->
+      with exn when noncritical exn ->
         Proofview.tclZERO exn
     in
     let rec try_red_apply thm_ty (exn0, info) =
@@ -1818,7 +1818,7 @@ let apply_list = function
 let find_matching_clause unifier clause =
   let rec find clause =
     try unifier clause
-    with e when catchable_exception e ->
+    with e when noncritical e ->
     try find (clenv_push_prod clause)
     with NotExtensibleClause -> failwith "Cannot apply"
   in find clause
@@ -4486,7 +4486,7 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ =
         error "Need a fully applied argument.";
       (* We lose the possibility of coercions in with-bindings *)
       pose_all_metas_as_evars env indclause.evd (clenv_value indclause)
-    with e when catchable_exception e ->
+    with e when noncritical e ->
     try find_clause (try_red_product env sigma typ)
     with Redelimination -> raise e in
   find_clause typ
@@ -5041,7 +5041,7 @@ let unify ?(state=TransparentState.full) x y =
     in
     let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in
     Proofview.Unsafe.tclEVARS sigma
-  with e when CErrors.noncritical e ->
+  with e when noncritical e ->
     Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None)))
   end
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 953faf6fdb..f2f3660520 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -484,7 +484,7 @@ let program_inference_hook env sigma ev =
     let c, _, ctx =
       Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac
     in Evd.set_universe_context sigma ctx, EConstr.of_constr c
-  with Logic_monad.TacticFailure e when Logic.catchable_exception e ->
+  with Logic_monad.TacticFailure e when noncritical e ->
     user_err Pp.(str "The statement obligations could not be resolved \
                       automatically, write a statement definition first.")