From b2c58a23a1f71c86d8a64147923214b5059bd747 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 8 Jan 2020 20:14:35 +0100
Subject: [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`.
---
 plugins/ltac/extratactics.mlg |  2 +-
 plugins/ltac/tacinterp.ml     | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'plugins/ltac')

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
-- 
cgit v1.2.3