diff options
| author | Maxime Dénès | 2018-01-13 09:21:31 -0800 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-13 09:21:31 -0800 |
| commit | 8ea2a8307a8d96f8275ebbd9bd4cbd1f6b0a00c6 (patch) | |
| tree | 160df8496eacfe12eac84279d01c91048197bf28 | |
| parent | 06b27c26e23a7f783c408535fe40565f3497abf5 (diff) | |
| parent | 23f9c7745a58d5a1727a1dfda0b2ad4cdc355ec8 (diff) | |
Merge PR #6578: Remove references to deleted Unicode.Unsupported exception
| -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 709ebeb7fd..b1e8efd8d1 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. *) |
