aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-13 09:21:31 -0800
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-13 09:21:31 -0800
commit8ea2a8307a8d96f8275ebbd9bd4cbd1f6b0a00c6 (patch)
tree160df8496eacfe12eac84279d01c91048197bf28 /kernel
parent06b27c26e23a7f783c408535fe40565f3497abf5 (diff)
parent23f9c7745a58d5a1727a1dfda0b2ad4cdc355ec8 (diff)
Merge PR #6578: Remove references to deleted Unicode.Unsupported exception
Diffstat (limited to 'kernel')
-rw-r--r--kernel/names.mli9
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. *)