diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-13 09:21:31 -0800 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-13 09:21:31 -0800 |
commit | 8ea2a8307a8d96f8275ebbd9bd4cbd1f6b0a00c6 (patch) | |
tree | 160df8496eacfe12eac84279d01c91048197bf28 /kernel | |
parent | 06b27c26e23a7f783c408535fe40565f3497abf5 (diff) | |
parent | 23f9c7745a58d5a1727a1dfda0b2ad4cdc355ec8 (diff) |
Merge PR #6578: Remove references to deleted Unicode.Unsupported exception
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/names.mli | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 709ebeb7f..b1e8efd8d 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -40,19 +40,16 @@ sig (** Hash over identifiers. *) val is_valid : string -> bool - (** Check that a string may be converted to an identifier. - @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) + (** Check that a string may be converted to an identifier. *) val of_bytes : bytes -> t val of_string : string -> t (** Converts a string into an identifier. - @raise UserError if the string is invalid as an identifier. - @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) + @raise UserError if the string is invalid as an identifier. *) val of_string_soft : string -> t (** Same as {!of_string} except that any string made of supported UTF-8 characters is accepted. - @raise UserError if the string is invalid as an UTF-8 string. - @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) + @raise UserError if the string is invalid as an UTF-8 string. *) val to_string : t -> string (** Converts a identifier into an string. *) |