[exninfo] Deprecate aliases for exception re-raising.

We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.

At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.

4 files changed, 12 insertions, 12 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b2ee0f9370..45fafd2872 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -520,7 +520,7 @@ let funind_purify f x =
   let st = Vernacstate.freeze_interp_state ~marshallable:false in
   try f x
   with e ->
-    let e = CErrors.push e in
+    let e = Exninfo.capture e in
     Vernacstate.unfreeze_interp_state st;
     Exninfo.iraise e
 
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 513f5ca77b..d0c94e7903 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -670,7 +670,7 @@ let hResolve id c occ t =
       Pretyping.understand env sigma t_hole
     with
       | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
-          let (e, info) = CErrors.push e in
+          let (e, info) = Exninfo.capture e in
           let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in
           resolve_hole (subst_hole_with_term loc_begin c_raw t_hole)
   in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6e620b71db..1d7fe335d1 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -165,8 +165,8 @@ let catching_error call_trace fail (e, info) =
 let catch_error call_trace f x =
   try f x
   with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    catching_error call_trace iraise e
+    let e = Exninfo.capture e in
+    catching_error call_trace Exninfo.iraise e
 
 let wrap_error tac k =
   if is_traced () then Proofview.tclORELSE tac k else tac
@@ -717,13 +717,13 @@ let interp_may_eval f ist env sigma = function
      try
         f ist env sigma c
      with reraise ->
-       let reraise = CErrors.push reraise in
+       let reraise = Exninfo.capture reraise in
        (* spiwack: to avoid unnecessary modifications of tacinterp, as this
           function already use effect, I call [run] hoping it doesn't mess
           up with any assumption. *)
        Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () ->
          str"interpretation of term " ++ pr_glob_constr_env env (fst c)));
-       iraise reraise
+       Exninfo.iraise reraise
 
 (* Interprets a constr expression possibly to first evaluate *)
 let interp_constr_may_eval ist env sigma c =
@@ -731,12 +731,12 @@ let interp_constr_may_eval ist env sigma c =
     try
       interp_may_eval interp_constr ist env sigma c
     with reraise ->
-      let reraise = CErrors.push reraise in
+      let reraise = Exninfo.capture reraise in
       (* spiwack: to avoid unnecessary modifications of tacinterp, as this
           function already use effect, I call [run] hoping it doesn't mess
           up with any assumption. *)
        Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"evaluation of term"));
-      iraise reraise
+      Exninfo.iraise reraise
   in
   begin
     (* spiwack: to avoid unnecessary modifications of tacinterp, as this
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index f95672a15d..6ff79ebb9b 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1095,11 +1095,11 @@ let tclDO n tac =
     try tac gl
     with
     | CErrors.UserError (l, s) as e ->
-        let _, info = CErrors.push e in
-        let e' = CErrors.UserError (l, prefix i ++ s) in
-        Util.iraise (e', info)
+      let _, info = Exninfo.capture e in
+      let e' = CErrors.UserError (l, prefix i ++ s) in
+      Exninfo.iraise (e', info)
     | Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s))  ->
-        raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
+      raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
   let rec loop i gl =
     if i = n then tac_err_at i gl else
     (tclTHEN (tac_err_at i) (loop (i + 1))) gl in