diff options
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index d82043da..92ee58f2 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -29,7 +29,11 @@ sig val of_string : string -> t (** Converts a string into an identifier. May raise [UserError _] if the - string is not valid. *) + string is not valid, or echo a warning if it contains invalid identifier + characters. *) + + val of_string_soft : string -> t + (** Same as {!of_string} except that no warning is ever issued. *) val to_string : t -> string (** Converts a identifier into an string. *) |