(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* status (** Return [None] if a given string can be used as a (Coq) identifier. Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. @raise Unsupported if the input string contains unsupported UTF-8 characters. *) val ident_refutation : string -> (bool * string) option (** First char of a string, converted to lowercase @raise Unsupported if the input string contains unsupported UTF-8 characters. @raise Assert_failure if the input string is empty. *) val lowercase_first_char : string -> string (** Return [true] if all UTF-8 characters in the input string are just plain ASCII characters. Returns [false] otherwise. *) val is_basic_ascii : string -> bool (** [ascii_of_ident s] maps UTF-8 string to a string composed solely from ASCII characters. The non-ASCII characters are translated to ["_UUxxxx_"] where {i xxxx} is the Unicode index of the character in hexadecimal (from four to six hex digits). To avoid potential name clashes, any preexisting substring ["_UU"] is turned into ["_UUU"]. *) val ascii_of_ident : string -> string (** Validate an UTF-8 string *) val is_utf8 : string -> bool