diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/impargs.ml | 4 | ||||
| -rw-r--r-- | interp/notation.ml | 4 |
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 |