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 /kernel/inductive.ml | |
| 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 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index c6035f78ff..1be86f2bf8 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -962,7 +962,7 @@ let check_one_fix renv recpos trees def = let stack_br = push_stack_args case_spec.(k) stack' in check_rec_call renv stack_br br') with (FixGuardError _ as exn) -> - let exn = CErrors.push exn in + let exn = Exninfo.capture exn in (* we try hard to reduce the match away by looking for a constructor in c_0 (we unfold definitions too) *) let c_0 = whd_all renv.env c_0 in @@ -1007,7 +1007,7 @@ let check_one_fix renv recpos trees def = check_nested_fix_body illformed renv' (decrArg+1) arg_sp body else check_rec_call renv' [] body) with (FixGuardError _ as exn) -> - let exn = CErrors.push exn in + let exn = Exninfo.capture exn in (* we try hard to reduce the fix away by looking for a constructor in l[decrArg] (we unfold definitions too) *) if List.length l <= decrArg then Exninfo.iraise exn; @@ -1055,7 +1055,7 @@ let check_one_fix renv recpos trees def = List.iter (check_rec_call renv []) l; check_rec_call renv [] c with (FixGuardError _ as exn) -> - let exn = CErrors.push exn in + let exn = Exninfo.capture exn in (* we try hard to reduce the proj away by looking for a constructor in c (we unfold definitions too) *) let c = whd_all renv.env c in |