(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* status (** Check whether a given string be used as a legal identifier. - [None] means yes - [Some (b,s)] means no, with explanation [s] and severity [b] *) val ident_refutation : string -> (bool * string) option (** First char of a string, converted to lowercase *) val lowercase_first_char : string -> string (** For extraction, turn a unicode string into an ascii-only one *) val is_basic_ascii : string -> bool val ascii_of_ident : string -> string