aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.mli
diff options
context:
space:
mode:
authorGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-01-11 18:38:41 +0900
committerGravatar GitHub <noreply@github.com>2018-01-11 18:38:41 +0900
commit23f9c7745a58d5a1727a1dfda0b2ad4cdc355ec8 (patch)
tree61b0ed7d00f6730a32306a6606ee8eba738197d6 /kernel/names.mli
parentd439c01190f45de5ac493b8f55d361503e83ad03 (diff)
Remove references to removed Unicode.Unsupported
Diffstat (limited to 'kernel/names.mli')
-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. *)