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`.
---
 proofs/refiner.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 832a749ef2..fd73ab1b5a 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -209,8 +209,8 @@ let catch_failerror (e, info) =
   | FailError (0,_) ->
       Control.check_for_interrupt ()
   | FailError (lvl,s) ->
-    iraise (FailError (lvl - 1, s), info)
-  | e -> iraise (e, info)
+    Exninfo.iraise (FailError (lvl - 1, s), info)
+  | e -> Exninfo.iraise (e, info)
   (** FIXME: do we need to add a [Errors.push] here? *)
 
 (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
@@ -219,7 +219,7 @@ let tclORELSE0 t1 t2 g =
     t1 g
   with (* Breakpoint *)
     | e when CErrors.noncritical e ->
-      let e = CErrors.push e in catch_failerror e; t2 g
+      let e = Exninfo.capture e in catch_failerror e; t2 g
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
    then applies t2 *)
@@ -232,7 +232,7 @@ let tclORELSE_THEN t1 t2then t2else gls =
   match
     try Some(tclPROGRESS t1 gls)
     with e when CErrors.noncritical e ->
-      let e = CErrors.push e in catch_failerror e; None
+      let e = Exninfo.capture e in catch_failerror e; None
   with
     | None -> t2else gls
     | Some sgl ->
-- 
cgit v1.2.3