aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-01-08 20:14:35 +0100
committerEmilio Jesus Gallego Arias2020-03-03 16:54:16 -0500
commitb2c58a23a1f71c86d8a64147923214b5059bd747 (patch)
treeea91b763facc24df188bd481b7a60e238f7a60a2 /interp
parent18aa9ca60ec9b3d1712276ec0c615dfe54c1a251 (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 'interp')
-rw-r--r--interp/impargs.ml4
-rw-r--r--interp/notation.ml4
2 files changed, 4 insertions, 4 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 78c4b21920..1365b97d82 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -77,9 +77,9 @@ let with_implicit_protection f x =
implicit_args := oflags;
rslt
with reraise ->
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
let () = implicit_args := oflags in
- iraise reraise
+ Exninfo.iraise reraise
type on_trailing_implicit = Error | Info | Silent
diff --git a/interp/notation.ml b/interp/notation.ml
index 2086e08f79..b869cb2a36 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1959,6 +1959,6 @@ let with_notation_protection f x =
let fs = freeze ~marshallable:false in
try let a = f x in unfreeze fs; a
with reraise ->
- let reraise = CErrors.push reraise in
+ let reraise = Exninfo.capture reraise in
let () = unfreeze fs in
- iraise reraise
+ Exninfo.iraise reraise