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

Reviewed-by: Matafou
Reviewed-by: ppedrot

3 files changed, 10 insertions, 9 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index ce054d2af2..f6b173968f 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -47,9 +47,9 @@ let load_rcfile ~rcfile ~state =
                          " found. Skipping rcfile loading."))
         *)
     with reraise ->
-      let reraise = CErrors.push reraise in
+      let reraise = Exninfo.capture reraise in
       let () = Feedback.msg_info (str"Load of rcfile failed.") in
-      iraise reraise
+      Exninfo.iraise reraise
 
 (* Recursively puts `.v` files in the LoadPath *)
 let build_stdlib_vo_path ~unix_path ~coq_path =
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index e4508e9bfc..b0012f8978 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -265,7 +265,7 @@ let read_sentence ~state input =
   let open Vernac.State in
   try Stm.parse_sentence ~doc:state.doc state.sid ~entry:G_toplevel.vernac_toplevel input
   with reraise ->
-    let reraise = CErrors.push reraise in
+    let reraise = Exninfo.capture reraise in
     discard_to_dot ();
     (* The caller of read_sentence does the error printing now, this
        should be re-enabled once we rely on the feedback error
@@ -360,7 +360,7 @@ let top_goal_print ~doc c oldp newp =
     end
   with
   | exn ->
-    let (e, info) = CErrors.push exn in
+    let (e, info) = Exninfo.capture exn in
     let loc = Loc.get_loc info in
     let msg = CErrors.iprint (e, info) in
     TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer
@@ -484,7 +484,7 @@ let read_and_execute ~state =
     TopErr.print_error_for_buffer Feedback.Error msg top_buffer;
     exit 1
   | any ->
-    let (e, info) = CErrors.push any in
+    let (e, info) = Exninfo.capture any in
     let loc = Loc.get_loc info in
     let msg = CErrors.iprint (e, info) in
     TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index adcce67b0d..8e6cd8f4c7 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -69,7 +69,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
       let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in
       { state with doc = ndoc; sid = nsid; proof = new_proof; }
     with reraise ->
-      let (reraise, info) = CErrors.push reraise in
+      let (reraise, info) = Exninfo.capture reraise in
       (* XXX: In non-interactive mode edit_at seems to do very weird
          things, so we better avoid it while we investigate *)
       if interactive then ignore(Stm.edit_at ~doc:state.doc state.sid);
@@ -77,7 +77,8 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) =
         match Loc.get_loc info with
         | None   -> Option.cata (Loc.add_loc info) info loc
         | Some _ -> info
-      end in iraise (reraise, info)
+      end in
+      Exninfo.iraise (reraise, info)
 
 (* Load a vernac file. CErrors are annotated with file and location *)
 let load_vernac_core ~echo ~check ~interactive ~state file =
@@ -113,9 +114,9 @@ let load_vernac_core ~echo ~check ~interactive ~state file =
   in
   try loop state []
   with any ->   (* whatever the exception *)
-    let (e, info) = CErrors.push any in
+    let (e, info) = Exninfo.capture any in
     input_cleanup ();
-    iraise (e, info)
+    Exninfo.iraise (e, info)
 
 let process_expr ~state loc_ast =
   interp_vernac ~interactive:true ~check:true ~state loc_ast