Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.

Reviewed-by: Matafou
Reviewed-by: ppedrot

6 files changed, 14 insertions, 14 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 1e18028e7b..86e6a92a22 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -97,8 +97,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
        which is an error irrelevant to the proof system (in fact it
        means that [e] comes from [tac] failing to yield enough
        success). Hence it reraises [e]. *)
-    let (_, info) = CErrors.push src in
-    iraise (e, info)
+    let (_, info) = Exninfo.capture src in
+    Exninfo.iraise (e, info)
   in
   let body, effs = Future.force const.Declare.proof_entry_body in
   (* We drop the side-effects from the entry, they already exist in the ambient environment *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 28feeecb86..e49f5abb8c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -236,7 +236,7 @@ let unify_resolve_refine poly flags gl clenv =
          Tacticals.New.tclZEROMSG (str "Unable to unify")
       | e when CErrors.noncritical e ->
          Tacticals.New.tclZEROMSG (str "Unexpected error")
-      | _ -> iraise ie)
+      | _ -> Exninfo.iraise ie)
 
 (** Dealing with goals of the form A -> B and hints of the form
   C -> A -> B.
@@ -770,7 +770,7 @@ module Search = struct
              (fun e' ->
               if CErrors.noncritical (fst e') then
                 (pr_error e'; aux (merge_exceptions e e') tl)
-              else iraise e')
+              else Exninfo.iraise e')
     and aux e = function
       | x :: xs -> onetac e x xs
       | [] ->
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 9a1e6a6736..aca6b4734a 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -235,7 +235,7 @@ module SearchProblem = struct
 (* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
               (lgls, cost, pptac) :: aux tacl
           with e when CErrors.noncritical e ->
-            let e = CErrors.push e in
+            let e = Exninfo.capture e in
             Refiner.catch_failerror e; aux tacl
     in aux l
 
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index dbabc4e4e0..7cdfd0637a 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -130,8 +130,8 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~
     | _ ->
       CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
   with reraise ->
-    let reraise = CErrors.push reraise in
-    iraise reraise
+    let reraise = Exninfo.capture reraise in
+    Exninfo.iraise reraise
 
 let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac =
   let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
@@ -160,8 +160,8 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
     try Proof.run_tactic env tac prf
     with Logic_monad.TacticFailure e as src ->
       (* Catch the inner error of the monad tactic *)
-      let (_, info) = CErrors.push src in
-      iraise (e, info)
+      let (_, info) = Exninfo.capture src in
+      Exninfo.iraise (e, info)
   in
   (* Plug back the retrieved sigma *)
   let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 4b93b81d1c..5fde6d2178 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -144,7 +144,7 @@ module New : sig
 
   (** [catch_failerror e] fails and decreases the level if [e] is an
       Ltac error with level more than 0. Otherwise succeeds. *)
-  val catch_failerror : Util.iexn -> unit tactic
+  val catch_failerror : Exninfo.iexn -> unit tactic
 
   val tclIDTAC : unit tactic
   val tclTHEN : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8371da76b2..83423b7556 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1848,12 +1848,12 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with e when CErrors.noncritical e ->
-    let e' = CErrors.push e in
+    let e' = Exninfo.capture e in
     try aux (clenv_push_prod clause)
     with NotExtensibleClause ->
       match e with
       | UnableToApply -> explain_unable_to_apply_lemma ?loc env sigma thm innerclause
-      | _ -> iraise e'
+      | _ -> Exninfo.iraise e'
   in
   aux (make_clenv_binding env sigma (d,thm) lbind)
 
@@ -1886,7 +1886,7 @@ let apply_in_once ?(respect_opaque = false) with_delta
             tac id
           ])
     with e when with_destruct && CErrors.noncritical e ->
-      let (e, info) = CErrors.push e in
+      let (e, info) = Exninfo.capture e in
         (descend_in_conjunctions (Id.Set.singleton targetid)
            (fun b id -> aux (id::idstoclear) b (mkVar id))
            (e, info) c)
@@ -3155,7 +3155,7 @@ let clear_for_destruct ids =
     (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids)
     (function
      | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT ()
-     | e -> iraise e)
+     | e -> Exninfo.iraise e)
 
 (* Either unfold and clear if defined or simply clear if not a definition *)
 let expand_hyp id =