diff options
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/util.mli b/lib/util.mli index 2f1a03a19c..1417d6dfcb 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -119,8 +119,10 @@ val delayed_force : 'a delayed -> 'a (** {6 Enriched exceptions} *) type iexn = Exninfo.iexn +[@@ocaml.deprecated "please use [Exninfo.iexn]"] -val iraise : iexn -> 'a +val iraise : Exninfo.iexn -> 'a +[@@ocaml.deprecated "please use [Exninfo.iraise]"] (** {6 Misc. } *) |