diff options
| author | Pierre-Marie Pédrot | 2020-03-04 11:25:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-04 11:25:51 +0100 |
| commit | 89f111f2e15d8cab61495a419f0c9f7ae95e086a (patch) | |
| tree | 300ebf99c79fe0e91faf2ad50439b17916e60cf7 /proofs | |
| parent | 2937fe5c1bb14a7cb7f00bb6e8d418ece00a7f50 (diff) | |
| parent | b2c58a23a1f71c86d8a64147923214b5059bd747 (diff) | |
Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.
Reviewed-by: Matafou
Reviewed-by: ppedrot
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 -> |