diff options
author | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-01-11 18:38:41 +0900 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-11 18:38:41 +0900 |
commit | 23f9c7745a58d5a1727a1dfda0b2ad4cdc355ec8 (patch) | |
tree | 61b0ed7d00f6730a32306a6606ee8eba738197d6 /kernel | |
parent | d439c01190f45de5ac493b8f55d361503e83ad03 (diff) |
Remove references to removed Unicode.Unsupported
This exception was removed in
[on Oct 13, 2016](https://github.com/coq/coq/commit/57c6ffd23836364168ffd1c66dbddbecf830c7c6#diff-297bc4c11289c2c0ed18d5eebf817c47).
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. *) |