diff options
| author | Emilio Jesus Gallego Arias | 2017-05-24 17:24:46 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-05-24 17:41:21 +0200 |
| commit | 6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 (patch) | |
| tree | b8a60ea2387f14a415d53a3cd9db516e384a5b4f /kernel/names.mli | |
| parent | a02f76f38592fd84cabd34102d38412f046f0d1b (diff) | |
| parent | 28f8da9489463b166391416de86420c15976522f (diff) | |
Merge branch 'trunk' into located_switch
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 be9b9422b7..5b0163aa55 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 |
