aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.ml
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 /pretyping/reductionops.ml
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 'pretyping/reductionops.ml')
-rw-r--r--pretyping/reductionops.ml2
1 files changed, 1 insertions, 1 deletions
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