diff options
Diffstat (limited to 'lib/util.mli')
| -rw-r--r-- | lib/util.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli index 068ea256f..d7194e389 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -39,6 +39,7 @@ val dummy_loc : loc val anomaly_loc : loc * string * std_ppcmds -> 'a val user_err_loc : loc * string * std_ppcmds -> 'a val invalid_arg_loc : loc * string -> 'a +val join_loc : loc -> loc -> loc (*s Chars. *) |