Merge PR #11735: Deprecating catchable_exception

Reviewed-by: ejgallego
Reviewed-by: ppedrot

15 files changed, 51 insertions, 50 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index d5938713d6..9088df6856 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,13 @@
 
 ### ML API
 
+Refiner.catchable_exception is deprecated, use instead
+CErrors.noncritical in try-with block. Note that nothing is needed in
+tclORELSE block since the exceptions there are supposed to be
+non-critical by construction.
+
+### ML API
+
 Types `precedence`, `parenRelation`, `tolerability` in
 `notgram_ops.ml` have been reworked. See `entry_level` and
 `entry_relative_level` in `constrexpr.ml`.
diff --git a/engine/proofview.ml b/engine/proofview.ml
index e4b6de627b..2e036be9e3 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -262,6 +262,8 @@ module Monad = Proof
 
 (** [tclZERO e] fails with exception [e]. It has no success. *)
 let tclZERO ?info e =
+  if not (CErrors.noncritical e) then
+    CErrors.anomaly (Pp.str "tclZERO receiving critical error: " ++ CErrors.print e);
   let info = match info with
   | None -> Exninfo.null
   | Some info -> info
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 8b6ddd1874..d0a2b37a69 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -186,24 +186,26 @@ module Monad : Monad.S with type +'a t = 'a tactic
 
 (** {7 Failure and backtracking} *)
 
-(** [tclZERO e] fails with exception [e]. It has no success. *)
+(** [tclZERO e] fails with exception [e]. It has no success.
+    Exception is supposed to be non critical *)
 val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic
 
 (** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
     the successes of [t1] have been depleted and it failed with [e],
     then it behaves as [t2 e]. In other words, [tclOR] inserts a
-    backtracking point. *)
+    backtracking point. In [t2], exception can be assumed non critical. *)
 val tclOR : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
 
 (** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one
     success or [t2 e] if [t1] fails with [e]. It is analogous to
     [try/with] handler of exception in that it is not a backtracking
-    point. *)
+    point. In [t2], exception can be assumed non critical. *)
 val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
 
 (** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
     succeeds at least once then it behaves as [tclBIND a s] otherwise,
-    if [a] fails with [e], then it behaves as [f e]. *)
+    if [a] fails with [e], then it behaves as [f e]. In [f]
+    exception can be assumed non critical. *)
 val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic
 
 (** [tclONCE t] behave like [t] except it has at most one success:
@@ -212,8 +214,9 @@ val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -
 val tclONCE : 'a tactic -> 'a tactic
 
 (** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
-    success. Otherwise it fails. The tactic [t] is run until its first
-    success, then a failure with exception [e] is simulated. It [t]
+    success. Otherwise it fails. The tactic [t] is run until its
+    first success, then a failure with exception [e] is
+    simulated ([e] has to be non critical). If [t]
     yields another success, then [tclEXACTLY_ONCE e t] fails with
     [MoreThanOneSuccess] (it is a user error). Otherwise,
     [tclEXACTLY_ONCE e t] succeeds with the first success of
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 69ab23aa55..321b05b97c 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 762f858b82..597c3fdaac 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/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index eeefeeb4f8..5fbea4eeef 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -229,9 +229,7 @@ let debug_prompt lev tac f =
       Proofview.tclTHEN
         (Proofview.tclLIFT begin
           (skip:=0) >> (skipped:=0) >>
-            if Logic.catchable_exception reraise then
-              msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ explain_logic_error reraise)
-            else return ()
+          msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ explain_logic_error reraise)
         end)
         (Proofview.tclZERO ~info reraise)
     end
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 4cec2c5a52..2eef459217 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/proofs/logic.mli b/proofs/logic.mli
index 5342b94b3e..ef8b2731b2 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -50,6 +50,7 @@ exception RefinerError of Environ.env * evar_map * refiner_error
 val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a
 
 val catchable_exception : exn -> bool
+[@@ocaml.deprecated "This function does not scale in the presence of dynamically added exceptions. Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."]
 
 (** Move destination for hypothesis *)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 2ef54540ff..75c3436cf4 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -204,14 +204,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
 
 
 let catch_failerror (e, info) =
-  if catchable_exception e then Control.check_for_interrupt ()
-  else match e with
-  | FailError (0,_) ->
-      Control.check_for_interrupt ()
-  | FailError (lvl,s) ->
+  match e with
+  | FailError (lvl,s) when lvl > 0 ->
     Exninfo.iraise (FailError (lvl - 1, s), info)
-  | e -> Exninfo.iraise (e, info)
-  (** FIXME: do we need to add a [Errors.push] here? *)
+  | e -> Control.check_for_interrupt ()
 
 (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
 let tclORELSE0 t1 t2 g =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index d9009da455..92d56d2904 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -189,7 +189,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
   Proofview.Goal.enter begin fun gls ->
     let resolve =
       try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
-      with e -> Proofview.tclZERO e
+      with e when noncritical e -> Proofview.tclZERO e
     in resolve >>= fun clenv' ->
        Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
   end
@@ -234,9 +234,8 @@ let unify_resolve_refine poly flags gl clenv =
       match fst ie with
       | Evarconv.UnableToUnify _ ->
          Tacticals.New.tclZEROMSG (str "Unable to unify")
-      | e when CErrors.noncritical e ->
-         Tacticals.New.tclZEROMSG (str "Unexpected error")
-      | _ -> Exninfo.iraise ie)
+      | e ->
+         Tacticals.New.tclZEROMSG (str "Unexpected error"))
 
 (** Dealing with goals of the form A -> B and hints of the form
   C -> A -> B.
@@ -459,7 +458,7 @@ let cut_of_hints h =
 
 let catchable = function
   | Refiner.FailError _ -> true
-  | e -> Logic.catchable_exception e
+  | e -> Logic.catchable_exception e [@@ocaml.warning "-3"]
 
 let pr_depth l =
   let rec fmt elts =
@@ -785,9 +784,7 @@ module Search = struct
              (with_shelf tac >>= fun s ->
               let i = !idx in incr idx; result s i None)
              (fun e' ->
-              if CErrors.noncritical (fst e') then
-                (pr_error e'; aux (merge_exceptions e e') tl)
-              else Exninfo.iraise e')
+                (pr_error e'; aux (merge_exceptions e e') tl))
     and aux e = function
       | x :: xs -> onetac e x xs
       | [] ->
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index c484191a6f..e26338436d 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -16,6 +16,7 @@ open EConstr
 val typeclasses_db : string
 
 val catchable : exn -> bool
+[@@ocaml.deprecated "Use instead CErrors.noncritical, or the exact name of the exception that matters in the corresponding case."]
 
 val set_typeclasses_debug : bool -> unit
 val get_typeclasses_debug : unit -> bool
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6e859d997b..49645d82a4 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 =
@@ -1627,10 +1627,9 @@ let try_rewrite tac =
   Proofview.tclORELSE tac begin function (e, info) -> match e with
     | Constr_matching.PatternMatchingFailure ->
         tclZEROMSG (str "Not a primitive equality here.")
-    | e when catchable_exception e ->
+    | e ->
         tclZEROMSG
           (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
-    | e -> Proofview.tclZERO ~info e
   end
 
 let cutSubstClause l2r eqn cls =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index ffa54bab93..a907b9e783 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -926,7 +926,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 c5cd98d386..30ca024a2f 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 1fb1416606..e2fdae37fb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -477,7 +477,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.")