diff options
Diffstat (limited to 'lib/interface.mli')
| -rw-r--r-- | lib/interface.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/interface.mli b/lib/interface.mli index 24f2b65249..a01ec20aed 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -236,7 +236,7 @@ type handle_exn_rty = state_id * location * string (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string (* spiwack: [Inl] for safe and [Inr] for unsafe. *) -type interp_rty = (string,string) Util.union +type interp_rty = state_id * (string,string) Util.union type handler = { |