diff options
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index be9b9422b..5b0163aa5 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -46,11 +46,12 @@ sig val of_bytes : bytes -> t val of_string : string -> t (** Converts a string into an identifier. - @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters. + @raise UserError if the string is invalid as an identifier. @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) val of_string_soft : string -> t - (** Same as {!of_string} except that no warning is ever issued. + (** 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. *) val to_string : t -> string |