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

Reviewed-by: Matafou
Reviewed-by: ppedrot

12 files changed, 27 insertions, 27 deletions

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index e57c324c9a..2b6f987fa6 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -37,9 +37,9 @@ module Hook = struct
   let call ?hook ?fix_exn x =
     try Option.iter (fun hook -> CEphemeron.get hook x) hook
     with e when CErrors.noncritical e ->
-      let e = CErrors.push e in
+      let e = Exninfo.capture e in
       let e = Option.cata (fun fix -> fix e) e fix_exn in
-      Util.iraise e
+      Exninfo.iraise e
 end
 
 (* Locality stuff *)
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index c816a4eb4f..e645fc552b 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -935,9 +935,9 @@ let protect_summaries f =
   try f fs
   with reraise ->
     (* Something wrong: undo the whole process *)
-    let reraise = CErrors.push reraise in
+    let reraise = Exninfo.capture reraise in
     let () = Summary.unfreeze_summaries fs in
-    iraise reraise
+    Exninfo.iraise reraise
 
 let start_module export id args res =
   protect_summaries (RawModOps.start_module export id args res)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 227d2f1554..80616ecc2a 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -118,7 +118,7 @@ let alarm what internal msg =
 let try_declare_scheme what f internal names kn =
   try f internal names kn
   with e ->
-  let e = CErrors.push e in
+  let e = Exninfo.capture e in
   let rec extract_exn = function Logic_monad.TacticFailure e -> extract_exn e | e -> e in
   let msg = match extract_exn (fst e) with
     | ParameterWithoutEquality cst ->
@@ -166,11 +166,11 @@ let try_declare_scheme what f internal names kn =
     | e when CErrors.noncritical e ->
         alarm what internal
           (str "Unexpected error during scheme creation: " ++ CErrors.print e)
-    | _ -> iraise e
+    | _ -> Exninfo.iraise e
   in
   match msg with
   | None -> ()
-  | Some msg -> iraise (UserError (None, msg), snd e)
+  | Some msg -> Exninfo.iraise (UserError (None, msg), snd e)
 
 let beq_scheme_msg mind =
   let mib = Global.lookup_mind mind in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index f7606f4ede..68f4f55d0e 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -375,8 +375,8 @@ let finish_proved env sigma idopt po info =
       (* This takes care of the implicits and hook for the current constant*)
       process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms
     with e when CErrors.noncritical e ->
-      let e = CErrors.push e in
-      iraise (fix_exn e)
+      let e = Exninfo.capture e in
+      Exninfo.iraise (fix_exn e)
     in ()
   | _ ->
     CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term")
diff --git a/vernac/library.ml b/vernac/library.ml
index 0f7e7d2aa0..5aff86c50c 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -440,11 +440,11 @@ let save_library_base f sum lib univs tasks proofs =
     System.marshal_out_segment f ch (proofs : seg_proofs);
     close_out ch
   with reraise ->
-    let reraise = CErrors.push reraise in
+    let reraise = Exninfo.capture reraise in
     close_out ch;
     Feedback.msg_warning (str "Removed file " ++ str f);
     Sys.remove f;
-    iraise reraise
+    Exninfo.iraise reraise
 
 type ('document,'counters) todo_proofs =
  | ProofsTodoNone (* for .vo *)
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 3937f887ad..fedebc9700 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1466,9 +1466,9 @@ let with_lib_stk_protection f x =
   let fs = Lib.freeze () in
   try let a = f x in Lib.unfreeze fs; a
   with reraise ->
-    let reraise = CErrors.push reraise in
+    let reraise = Exninfo.capture reraise in
     let () = Lib.unfreeze fs in
-    iraise reraise
+    Exninfo.iraise reraise
 
 let with_syntax_protection f x =
   with_lib_stk_protection
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 76dbf1ad5a..27eb821a6a 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -428,7 +428,7 @@ let solve_by_tac ?loc name evi t poly ctx =
     Some (body, entry.Declare.proof_entry_type, ctx')
   with
   | Refiner.FailError (_, s) as exn ->
-    let _ = CErrors.push exn in
+    let _ = Exninfo.capture exn in
     user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
   (* If the proof is open we absorb the error and leave the obligation open *)
   | Proof.OpenProof _ ->
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index de02f7ecfb..509c164af8 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -361,7 +361,7 @@ let in_phase ~phase f x =
   with exn ->
     let iexn = Exninfo.capture exn in
     default_phase := op;
-    Util.iraise iexn
+    Exninfo.iraise iexn
 
 let pr_loc loc =
     let fname = loc.Loc.fname in
@@ -394,7 +394,7 @@ let pr_phase ?loc () =
      None
 
 let print_err_exn any =
-  let (e, info) = CErrors.push any in
+  let (e, info) = Exninfo.capture any in
   let loc = Loc.get_loc info in
   let pre_hdr = pr_phase ?loc () in
   let msg = CErrors.iprint (e, info) ++ fnl () in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 3cf4b4a89d..953faf6fdb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -342,9 +342,9 @@ let dump_universes_gen prl g s =
     close ();
     str "Universes written to file \"" ++ str s ++ str "\"."
   with reraise ->
-    let reraise = CErrors.push reraise in
+    let reraise = Exninfo.capture reraise in
     close ();
-    iraise reraise
+    Exninfo.iraise reraise
 
 let universe_subgraph ?loc g univ =
   let open Univ in
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index f41df06f85..e0afb7f483 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -109,11 +109,11 @@ let type_vernac opn converted_args ~atts =
     phase := "Executing command";
     hunk ~atts
   with
-    | reraise ->
-        let reraise = CErrors.push reraise in
-        if !Flags.debug then
-          Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase);
-        iraise reraise
+  | reraise ->
+    let reraise = Exninfo.capture reraise in
+    if !Flags.debug then
+      Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase);
+    Exninfo.iraise reraise
 
 (** VERNAC EXTEND registering *)
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1ec09b6beb..8083098022 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -96,7 +96,7 @@ let with_fail f : (Pp.t, unit) result =
   (* Fail Timeout is a common pattern so we need to support it. *)
   | e when CErrors.noncritical e || e = CErrors.Timeout ->
     (* The error has to be printed in the failing state *)
-    Ok CErrors.(iprint (push e))
+    Ok CErrors.(iprint (Exninfo.capture e))
 
 (* We restore the state always *)
 let with_fail ~st f =
@@ -262,10 +262,10 @@ let interp_gen ~verbosely ~st ~interp_fn cmd =
       Vernacstate.freeze_interp_state ~marshallable:false
     ) st
   with exn ->
-    let exn = CErrors.push exn in
+    let exn = Exninfo.capture exn in
     let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in
     Vernacstate.invalidate_cache ();
-    Util.iraise exn
+    Exninfo.iraise exn
 
 (* Regular interp *)
 let interp ?(verbosely=true) ~st cmd =
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 3c70961e06..59557a60a6 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -21,7 +21,7 @@ module Parser = struct
     Flags.with_option Flags.we_are_parsing (fun () ->
       try Pcoq.Entry.parse entry pa
       with e when CErrors.noncritical e ->
-        let (e, info) = CErrors.push e in
+        let (e, info) = Exninfo.capture e in
         Exninfo.iraise (e, info))
     ()