diff options
| author | Emilio Jesus Gallego Arias | 2020-01-08 20:14:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-03 16:54:16 -0500 |
| commit | b2c58a23a1f71c86d8a64147923214b5059bd747 (patch) | |
| tree | ea91b763facc24df188bd481b7a60e238f7a60a2 /proofs | |
| parent | 18aa9ca60ec9b3d1712276ec0c615dfe54c1a251 (diff) | |
[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`.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/refiner.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 -> |