[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, 13 insertions, 14 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 55c1f41c2c..afe776dced 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -73,11 +73,11 @@ let error_wrong_numarg_inductive ?loc env c n =
 
 let list_try_compile f l =
   let rec aux errors = function
-  | [] -> if errors = [] then anomaly (str "try_find_f.") else iraise (List.last errors)
+  | [] -> if errors = [] then anomaly (str "try_find_f.") else Exninfo.iraise (List.last errors)
   | h::t ->
       try f h
       with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e ->
-            let e = CErrors.push e in
+            let e = Exninfo.capture e in
             aux (e::errors) t in
   aux [] l
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ac1a4e88ef..1269488af3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -87,9 +87,9 @@ let search_guard ?loc env possible_indexes fixdefs =
     let fix = ((indexes, 0),fixdefs) in
     (try check_fix env fix
      with reraise ->
-       let (e, info) = CErrors.push reraise in
+       let (e, info) = Exninfo.capture reraise in
        let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
-       iraise (e, info));
+       Exninfo.iraise (e, info));
     indexes
   else
     (* we now search recursively among all combinations *)
@@ -266,8 +266,8 @@ let apply_heuristics env sigma fail_evar =
   let flags = default_flags_of (Typeclasses.classes_transparent_state ()) in
   try solve_unif_constraints_with_heuristics ~flags env sigma
   with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    if fail_evar then iraise e else sigma
+    let e = Exninfo.capture e in
+    if fail_evar then Exninfo.iraise e else sigma
 
 let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen =
   (* Naive way, call resolution again with failure flag *)
@@ -753,9 +753,9 @@ struct
           let cofix = (i, fixdecls) in
             (try check_cofix !!env (i, nf_fix sigma fixdecls)
              with reraise ->
-               let (e, info) = CErrors.push reraise in
+               let (e, info) = Exninfo.capture reraise in
                let info = Option.cata (Loc.add_loc info) info loc in
-               iraise (e, info));
+               Exninfo.iraise (e, info));
             make_judge (mkCoFix cofix) ftys.(i)
       in
       discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma fixj tycon
@@ -946,9 +946,9 @@ struct
       try
         judge_of_product !!env name j j'
       with TypeError _ as e ->
-        let (e, info) = CErrors.push e in
+        let (e, info) = Exninfo.capture e in
         let info = Option.cata (Loc.add_loc info) info loc in
-        iraise (e, info) in
+        Exninfo.iraise (e, info) in
       discard_trace @@ inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon
 
   let pretype_letin self (name, c1, t, c2) =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 98eb33273f..b07ae8788a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1465,7 +1465,7 @@ let report_anomaly (e, info) =
       UserError (None, msg)
     else e
   in
-  iraise (e, info)
+  Exninfo.iraise (e, info)
 
 let f_conv ?l2r ?reds env ?evars x y =
   let inj = EConstr.Unsafe.to_constr in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5b87603d54..1df377b20e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1149,10 +1149,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     if !debug_unification then Feedback.msg_debug (str "Leaving unification with success");
     a
   with e ->
-    let e = CErrors.push e in
+    let e = Exninfo.capture e in
     if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure");
-    iraise e
-
+    Exninfo.iraise e
 
 let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env